Definition df-f 6540

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 7094, dff3 7095, and dff4 7096. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f	⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf 6532	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6531	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5662	. . . 4 class ran 𝐹
7	6, 2	wss 3904	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 400	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6683  feq2  6684  feq3  6685  nff  6701  sbcfg  6703  ffn  6705  dffn2  6707  frn  6713  dffn3  6718  ffrnb  6720  fss  6722  fcof  6729  funssxp  6734  fdmrn  6737  fun  6740  fnfco  6743  fssres  6744  fcoi2  6753  fint  6757  fin  6758  f0  6759  fconst  6764  f1ssr  6782  fof  6792  dff1o2  6826  dff2  7094  dff3  7095  fmpt  7105  ffnfv  7114  ffvresb  7121  idref  7142  fpr  7151  dff1o6  7273  fliftf  7313  fiun  7939  f1iun  7940  ffoss  7942  1stcof  8015  2ndcof  8016  smores  8338  smores2  8340  iordsmo  8343  sbthlem9  9082  inf3lem6  9601  alephsmo  10085  alephsing  10259  axdc3lem2  10434  smobeth  10570  fpwwe2lem10  10624  gruiun  10783  gruima  10786  nqerf  10914  om2uzf1oi  13988  fclim  15603  invf  17824  funcres2b  17953  funcres2c  17959  hofcllem  18313  hofcl  18314  nfchnd  18666  gsumval2  18743  resmgmhm2b  18770  resmhm2b  18880  frmdss2  18921  gsumval3a  19972  subgdmdprd  20105  srgfcl  20277  lsslindf  21959  indlcim  21969  cnrest2  23422  lmss  23434  conncn  23562  txflf  24142  cnextf  24202  clsnsg  24246  tgpconncomp  24249  psmetxrge0  24449  causs  25436  ellimc2  26015  perfdvf  26041  c1lip2  26136  dvne0  26149  plyeq0  26347  plyreres  26423  aannenlem1  26468  taylf  26500  ulmss  26536  elno2  27794  elno3  27795  cutsf  27961  madef  28005  oniso  28440  mpteleeOLD  29211  ausgrusgrb  29481  ausgrumgri  29483  usgrexmplef  29575  subuhgr  29602  subupgr  29603  subumgr  29604  subusgr  29605  upgrres  29622  umgrres  29623  hhssnv  31582  pjfi  32022  maprnin  33042  cycpmconjslem1  33440  esplyfv1  33925  measdivcstALTV  34581  sitgf  34703  eulerpartlemn  34737  reprinrn  34971  cvmlift2lem9a  35749  satff  35856  icoreresf  37942  poimirlem30  38245  poimirlem31  38246  isbnd3  38379  dihf11lem  41986  ofoafg  44029  ofoaid1  44033  ofoaid2  44034  naddcnff  44037  ntrf  44797  clsf2  44800  gneispace3  44807  gneispacef2  44810  k0004lem1  44821  dvsid  44989  stoweidlem27  46689  stoweidlem29  46691  stoweidlem31  46693  fourierdlem15  46784  mbfresmf  47401  sinnpoly  47573  ffnafv  47853  fcdmvafv2v  47918  iccpartf  48125  slotresfo  49622