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

Definition df-f 6353
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. 𝐹:𝐴𝐵 can be read as "𝐹 is a function from 𝐴 to 𝐵". For alternate definitions, see dff2 6858, dff3 6859, and dff4 6860. (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 6345 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 6344 . . 3 wff 𝐹 Fn 𝐴
63crn 5550 . . . 4 class ran 𝐹
76, 2wss 3935 . . 3 wff ran 𝐹𝐵
85, 7wa 396 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 207 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  feq1  6489  feq2  6490  feq3  6491  nff  6504  sbcfg  6506  ffn  6508  dffn2  6510  frn  6514  dffn3  6519  fss  6521  fco  6525  funssxp  6529  fdmrn  6532  fun  6534  fnfco  6537  fssres  6538  fcoi2  6547  fint  6552  fin  6553  f0  6554  fconst  6559  f1ssr  6575  fof  6584  dff1o2  6614  dff2  6858  dff3  6859  fmpt  6867  ffnfv  6875  ffvresb  6881  idref  6901  fpr  6909  dff1o6  7023  fliftf  7057  fiunw  7632  f1iunw  7633  fiun  7635  f1iun  7636  ffoss  7638  1stcof  7710  2ndcof  7711  smores  7980  smores2  7982  iordsmo  7985  sbthlem9  8624  inf3lem6  9085  alephsmo  9517  alephsing  9687  axdc3lem2  9862  smobeth  9997  fpwwe2lem11  10051  gruiun  10210  gruima  10213  nqerf  10341  om2uzf1oi  13311  fclim  14900  invf  17028  funcres2b  17157  funcres2c  17161  hofcllem  17498  hofcl  17499  gsumval2  17886  resmhm2b  17977  frmdss2  18018  gsumval3a  18954  subgdmdprd  19087  srgfcl  19196  lsslindf  20904  indlcim  20914  cnrest2  21824  lmss  21836  conncn  21964  txflf  22544  cnextf  22604  clsnsg  22647  tgpconncomp  22650  psmetxrge0  22852  causs  23830  ellimc2  24404  perfdvf  24430  c1lip2  24524  dvne0  24537  plyeq0  24730  plyreres  24801  aannenlem1  24846  taylf  24878  ulmss  24914  mptelee  26609  ausgrusgrb  26878  ausgrumgri  26880  usgrexmplef  26969  subuhgr  26996  subupgr  26997  subumgr  26998  subusgr  26999  upgrres  27016  umgrres  27017  hhssnv  28969  pjfi  29409  maprnin  30394  cycpmconjslem1  30724  measdivcstALTV  31384  sitgf  31505  eulerpartlemn  31539  reprinrn  31789  cvmlift2lem9a  32448  satff  32555  elno2  33059  elno3  33060  scutf  33171  icoreresf  34516  poimirlem30  34804  poimirlem31  34805  isbnd3  34945  dihf11lem  38284  ntrf  40353  clsf2  40356  gneispace3  40363  gneispacef2  40366  k0004lem1  40377  dvsid  40543  stoweidlem27  42193  stoweidlem29  42195  stoweidlem31  42197  fourierdlem15  42288  mbfresmf  42897  ffnafv  43251  frnvafv2v  43316  iccpartf  43438  resmgmhm2b  43914
  Copyright terms: Public domain W3C validator