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 5930
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 6411, dff3 6412, and dff4 6413. (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 5922 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 5921 . . 3 wff 𝐹 Fn 𝐴
63crn 5144 . . . 4 class ran 𝐹
76, 2wss 3607 . . 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  6064  feq2  6065  feq3  6066  nff  6079  sbcfg  6081  ffn  6083  dffn2  6085  frn  6091  dffn3  6092  fss  6094  fco  6096  funssxp  6099  fdmrn  6102  fun  6104  fnfco  6107  fssres  6108  fcoi2  6117  fint  6122  fin  6123  f0  6124  fconst  6129  f1ssr  6145  fof  6153  dff1o2  6180  dff2  6411  dff3  6412  fmpt  6421  ffnfv  6428  ffvresb  6434  fpr  6461  idref  6539  dff1o6  6571  fliftf  6605  fun11iun  7168  ffoss  7169  1stcof  7240  2ndcof  7241  smores  7494  smores2  7496  iordsmo  7499  sbthlem9  8119  sucdom2  8197  inf3lem6  8568  alephsmo  8963  alephsing  9136  axdc3lem2  9311  smobeth  9446  fpwwe2lem11  9500  gch3  9536  gruiun  9659  gruima  9662  nqerf  9790  om2uzf1oi  12792  fclim  14328  invf  16475  funcres2b  16604  funcres2c  16608  hofcllem  16945  hofcl  16946  gsumval2  17327  resmhm2b  17408  frmdss2  17447  gsumval3a  18350  subgdmdprd  18479  srgfcl  18561  lsslindf  20217  indlcim  20227  cnrest2  21138  lmss  21150  conncn  21277  txflf  21857  cnextf  21917  clsnsg  21960  tgpconncomp  21963  psmetxrge0  22165  causs  23142  ellimc2  23686  perfdvf  23712  c1lip2  23806  dvne0  23819  plyeq0  24012  plyreres  24083  aannenlem1  24128  taylf  24160  ulmss  24196  mptelee  25820  ausgrusgrb  26105  ausgrumgri  26107  usgrexmplef  26196  subuhgr  26223  subupgr  26224  subumgr  26225  subusgr  26226  upgrres  26243  umgrres  26244  hhssnv  28249  pjfi  28691  maprnin  29634  measdivcstOLD  30415  sitgf  30537  eulerpartlemn  30571  reprinrn  30824  cvmlift2lem9a  31411  elno2  31932  elno3  31933  scutf  32044  icoreresf  33330  poimirlem30  33569  poimirlem31  33570  isbnd3  33713  dihf11lem  36872  ntrf  38738  clsf2  38741  gneispace3  38748  gneispacef2  38751  gneispacern  38753  k0004lem1  38762  dvsid  38847  stoweidlem27  40562  stoweidlem29  40564  stoweidlem31  40566  fourierdlem15  40657  mbfresmf  41269  ffnafv  41572  iccpartf  41692  resmgmhm2b  42125
  Copyright terms: Public domain W3C validator