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

Definition df-f 6338
 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 6847, dff3 6848, and dff4 6849. (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 6330 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 6329 . . 3 wff 𝐹 Fn 𝐴
63crn 5533 . . . 4 class ran 𝐹
76, 2wss 3908 . . 3 wff ran 𝐹𝐵
85, 7wa 399 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 209 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  feq1  6475  feq2  6476  feq3  6477  nff  6490  sbcfg  6492  ffn  6494  dffn2  6496  frn  6500  dffn3  6506  fss  6508  fco  6512  funssxp  6516  fdmrn  6519  fun  6521  fnfco  6524  fssres  6525  fcoi2  6534  fint  6539  fin  6540  f0  6541  fconst  6546  f1ssr  6563  fof  6572  dff1o2  6602  dff2  6847  dff3  6848  fmpt  6856  ffnfv  6864  ffvresb  6870  idref  6890  fpr  6898  dff1o6  7015  fliftf  7052  fiun  7630  f1iun  7631  ffoss  7633  1stcof  7705  2ndcof  7706  smores  7976  smores2  7978  iordsmo  7981  sbthlem9  8623  inf3lem6  9084  alephsmo  9517  alephsing  9687  axdc3lem2  9862  smobeth  9997  fpwwe2lem11  10051  gruiun  10210  gruima  10213  nqerf  10341  om2uzf1oi  13316  fclim  14901  invf  17029  funcres2b  17158  funcres2c  17162  hofcllem  17499  hofcl  17500  gsumval2  17887  resmhm2b  17978  frmdss2  18019  gsumval3a  19014  subgdmdprd  19147  srgfcl  19256  lsslindf  20517  indlcim  20527  cnrest2  21889  lmss  21901  conncn  22029  txflf  22609  cnextf  22669  clsnsg  22713  tgpconncomp  22716  psmetxrge0  22918  causs  23900  ellimc2  24478  perfdvf  24504  c1lip2  24599  dvne0  24612  plyeq0  24806  plyreres  24877  aannenlem1  24922  taylf  24954  ulmss  24990  mptelee  26687  ausgrusgrb  26956  ausgrumgri  26958  usgrexmplef  27047  subuhgr  27074  subupgr  27075  subumgr  27076  subusgr  27077  upgrres  27094  umgrres  27095  hhssnv  29045  pjfi  29485  maprnin  30477  cycpmconjslem1  30827  measdivcstALTV  31558  sitgf  31679  eulerpartlemn  31713  reprinrn  31963  cvmlift2lem9a  32624  satff  32731  elno2  33235  elno3  33236  scutf  33347  icoreresf  34730  poimirlem30  35045  poimirlem31  35046  isbnd3  35180  dihf11lem  38520  ntrf  40759  clsf2  40762  gneispace3  40769  gneispacef2  40772  k0004lem1  40783  dvsid  40969  stoweidlem27  42608  stoweidlem29  42610  stoweidlem31  42612  fourierdlem15  42703  mbfresmf  43312  ffnafv  43666  frnvafv2v  43731  iccpartf  43887  resmgmhm2b  44359
 Copyright terms: Public domain W3C validator