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

Definition df-f 5493
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5917, dff3 5918, and dff4 5919. (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 5485 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 5484 . . 3 wff 𝐹 Fn 𝐴
63crn 4914 . . . 4 class ran 𝐹
76, 2wss 3309 . . 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  5611  feq2  5612  feq3  5613  nff  5624  ffn  5626  dffn2  5627  frn  5632  dffn3  5633  fss  5634  fco  5635  funssxp  5639  fun  5642  fnfco  5644  fssres  5645  fcoi2  5653  fint  5657  fin  5658  f0  5662  fconst  5664  f1ssr  5680  fof  5688  dff1o2  5714  fun11iun  5730  ffoss  5742  dff2  5917  dff3  5918  fmpt  5926  ffnfv  5930  ffvresb  5936  fpr  5950  idref  6015  dff1o6  6049  fliftf  6073  1stcof  6410  2ndcof  6411  smores  6650  smores2  6652  iordsmo  6655  map0e  7087  sbthlem9  7261  sucdom2  7339  inf3lem6  7624  alephsmo  8021  alephsing  8194  axdc3lem2  8369  smobeth  8499  fpwwe2lem11  8553  gch3  8589  gruiun  8712  gruima  8715  nqerf  8845  om2uzf1oi  11331  fclim  12385  invf  14031  funcres2b  14132  funcres2c  14136  hofcllem  14393  hofcl  14394  resmhm2b  14799  gsumval2  14821  frmdss2  14846  gsumval3a  15550  subgdmdprd  15630  cnrest  17387  cnrest2  17388  lmss  17400  concn  17527  txflf  18076  cnextf  18135  clsnsg  18177  tgpconcomp  18180  psmetxrge0  18382  causs  19289  ellimc2  19802  perfdvf  19828  c1lip2  19920  dvne0  19933  plyeq0  20168  plyreres  20238  aannenlem1  20283  taylf  20315  ulmss  20351  ausisusgra  21418  usgraedgrnv  21435  usgraexmpl  21458  cusgrarn  21506  hhssnv  22802  pjfi  23244  fdmrn  24074  measdivcstOLD  24613  sitgf  24695  cvmlift2lem9a  25025  elno2  25644  elno3  25645  nodenselem6  25676  mptelee  25869  isbnd3  26535  lsslindf  27389  indlcim  27399  dvsid  27637  stoweidlem27  27864  stoweidlem29  27866  stoweidlem31  27868  ffnafv  28123  sbcf  28189  uhgraedgrnv  28424  dihf11lem  32238
  Copyright terms: Public domain W3C validator