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 6045
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 6526, dff3 6527, and dff4 6528. (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 6037 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 6036 . . 3 wff 𝐹 Fn 𝐴
63crn 5259 . . . 4 class ran 𝐹
76, 2wss 3707 . . 3 wff ran 𝐹𝐵
85, 7wa 383 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 196 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  feq1  6179  feq2  6180  feq3  6181  nff  6194  sbcfg  6196  ffn  6198  dffn2  6200  frn  6206  dffn3  6207  fss  6209  fco  6211  funssxp  6214  fdmrn  6217  fun  6219  fnfco  6222  fssres  6223  fcoi2  6232  fint  6237  fin  6238  f0  6239  fconst  6244  f1ssr  6260  fof  6268  dff1o2  6295  dff2  6526  dff3  6527  fmpt  6536  ffnfv  6543  ffvresb  6549  fpr  6576  idref  6654  dff1o6  6686  fliftf  6720  fun11iun  7283  ffoss  7284  1stcof  7355  2ndcof  7356  smores  7610  smores2  7612  iordsmo  7615  sbthlem9  8235  sucdom2  8313  inf3lem6  8695  alephsmo  9107  alephsing  9282  axdc3lem2  9457  smobeth  9592  fpwwe2lem11  9646  gch3  9682  gruiun  9805  gruima  9808  nqerf  9936  om2uzf1oi  12938  fclim  14475  invf  16621  funcres2b  16750  funcres2c  16754  hofcllem  17091  hofcl  17092  gsumval2  17473  resmhm2b  17554  frmdss2  17593  gsumval3a  18496  subgdmdprd  18625  srgfcl  18707  lsslindf  20363  indlcim  20373  cnrest2  21284  lmss  21296  conncn  21423  txflf  22003  cnextf  22063  clsnsg  22106  tgpconncomp  22109  psmetxrge0  22311  causs  23288  ellimc2  23832  perfdvf  23858  c1lip2  23952  dvne0  23965  plyeq0  24158  plyreres  24229  aannenlem1  24274  taylf  24306  ulmss  24342  mptelee  25966  ausgrusgrb  26251  ausgrumgri  26253  usgrexmplef  26342  subuhgr  26369  subupgr  26370  subumgr  26371  subusgr  26372  upgrres  26389  umgrres  26390  hhssnv  28422  pjfi  28864  maprnin  29807  measdivcstOLD  30588  sitgf  30710  eulerpartlemn  30744  reprinrn  30997  cvmlift2lem9a  31584  elno2  32105  elno3  32106  scutf  32217  icoreresf  33503  poimirlem30  33744  poimirlem31  33745  isbnd3  33888  dihf11lem  37049  ntrf  38915  clsf2  38918  gneispace3  38925  gneispacef2  38928  gneispacern  38930  k0004lem1  38939  dvsid  39024  stoweidlem27  40739  stoweidlem29  40741  stoweidlem31  40743  fourierdlem15  40834  mbfresmf  41446  ffnafv  41749  iccpartf  41869  resmgmhm2b  42302
  Copyright terms: Public domain W3C validator