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 5861
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 6337, dff3 6338, and dff4 6339. (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 5853 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 5852 . . 3 wff 𝐹 Fn 𝐴
63crn 5085 . . . 4 class ran 𝐹
76, 2wss 3560 . . 3 wff ran 𝐹𝐵
85, 7wa 384 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 196 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  feq1  5993  feq2  5994  feq3  5995  nff  6008  sbcfg  6010  ffn  6012  dffn2  6014  frn  6020  dffn3  6021  fss  6023  fco  6025  funssxp  6028  fdmrn  6031  fun  6033  fnfco  6036  fssres  6037  fcoi2  6046  fint  6051  fin  6052  f0  6053  fconst  6058  f1ssr  6074  fof  6082  dff1o2  6109  dff2  6337  dff3  6338  fmpt  6347  ffnfv  6354  ffvresb  6360  fpr  6386  idref  6464  dff1o6  6496  fliftf  6530  fun11iun  7088  ffoss  7089  1stcof  7156  2ndcof  7157  smores  7409  smores2  7411  iordsmo  7414  sbthlem9  8038  sucdom2  8116  inf3lem6  8490  alephsmo  8885  alephsing  9058  axdc3lem2  9233  smobeth  9368  fpwwe2lem11  9422  gch3  9458  gruiun  9581  gruima  9584  nqerf  9712  om2uzf1oi  12708  fclim  14234  invf  16368  funcres2b  16497  funcres2c  16501  hofcllem  16838  hofcl  16839  gsumval2  17220  resmhm2b  17301  frmdss2  17340  gsumval3a  18244  subgdmdprd  18373  srgfcl  18455  lsslindf  20109  indlcim  20119  cnrest2  21030  lmss  21042  conncn  21169  txflf  21750  cnextf  21810  clsnsg  21853  tgpconncomp  21856  psmetxrge0  22058  causs  23036  ellimc2  23581  perfdvf  23607  c1lip2  23699  dvne0  23712  plyeq0  23905  plyreres  23976  aannenlem1  24021  taylf  24053  ulmss  24089  mptelee  25709  ausgrusgrb  25987  ausgrumgri  25989  usgrexmplef  26078  subuhgr  26105  subupgr  26106  subumgr  26107  subusgr  26108  hhssnv  28009  pjfi  28451  maprnin  29390  measdivcstOLD  30110  sitgf  30232  eulerpartlemn  30266  cvmlift2lem9a  31046  elno2  31561  elno3  31562  nodenselem6  31602  icoreresf  32871  poimirlem30  33110  poimirlem31  33111  isbnd3  33254  dihf11lem  36074  ntrf  37942  clsf2  37945  gneispace3  37952  gneispacef2  37955  gneispacern  37957  k0004lem1  37966  dvsid  38051  stoweidlem27  39581  stoweidlem29  39583  stoweidlem31  39585  fourierdlem15  39676  mbfresmf  40285  ffnafv  40585  iccpartf  40695  resmgmhm2b  41118
  Copyright terms: Public domain W3C validator