MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-f Structured version   GIF version

Definition df-f 5557
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5981, dff3 5982, and dff4 5983. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wf 5549 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 5548 . . 3 wff 𝐹 Fn 𝐴
63crn 4971 . . . 4 class ran 𝐹
76, 2wss 3350 . . 3 wff ran 𝐹𝐵
85, 7wa 360 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 178 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff set class
This definition is referenced by:  feq1  5675  feq2  5676  feq3  5677  nff  5688  ffn  5690  dffn2  5691  frn  5696  dffn3  5697  fss  5698  fco  5699  funssxp  5703  fun  5706  fnfco  5708  fssres  5709  fcoi2  5717  fint  5721  fin  5722  f0  5726  fconst  5728  f1ssr  5744  fof  5752  dff1o2  5778  fun11iun  5794  ffoss  5806  dff2  5981  dff3  5982  fmpt  5990  ffnfv  5994  ffvresb  5999  fpr  6014  idref  6079  dff1o6  6113  fliftf  6137  1stcof  6478  2ndcof  6479  smores  6709  smores2  6711  iordsmo  6714  map0e  7146  sbthlem9  7320  sucdom2  7398  inf3lem6  7683  alephsmo  8080  alephsing  8253  axdc3lem2  8428  smobeth  8558  fpwwe2lem11  8612  gch3  8648  gruiun  8771  gruima  8774  nqerf  8904  om2uzf1oi  11397  fclim  12467  invf  14113  funcres2b  14214  funcres2c  14218  hofcllem  14475  hofcl  14476  resmhm2b  14893  gsumval2  14915  frmdss2  14940  gsumval3a  15644  subgdmdprd  15724  cnrest  17481  cnrest2  17482  lmss  17494  concn  17621  txflf  18170  cnextf  18229  clsnsg  18271  tgpconcomp  18274  psmetxrge0  18476  causs  19383  ellimc2  19896  perfdvf  19922  c1lip2  20014  dvne0  20027  plyeq0  20262  plyreres  20332  aannenlem1  20377  taylf  20409  ulmss  20445  ausisusgra  21512  usgraedgrnv  21529  usgraexmpl  21552  cusgrarn  21600  hhssnv  22896  pjfi  23338  fdmrn  24186  maprnin  24276  measdivcstOLD  24936  sitgf  25025  eulerpartlemn  25056  cvmlift2lem9a  25456  elno2  26066  elno3  26067  nodenselem6  26098  mptelee  26291  isbnd3  26949  lsslindf  27799  indlcim  27809  dvsid  28047  stoweidlem27  28270  stoweidlem29  28272  stoweidlem31  28274  ffnafv  28530  sbcfg  28602  uhgraedgrnv  28957  dihf11lem  33113
  Copyright terms: Public domain W3C validator