Definition df-f 6529

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 7084, dff3 7085, and dff4 7086. (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 6521	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6520	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5653	. . . 4 class ran 𝐹
7	6, 2	wss 3907	. . 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  6673  feq2  6674  feq3  6675  nff  6691  sbcfg  6693  ffn  6695  dffn2  6697  frn  6703  dffn3  6708  ffrnb  6710  fss  6712  fcof  6719  funssxp  6724  fdmrn  6727  fun  6730  fnfco  6733  fssres  6734  fcoi2  6743  fint  6747  fin  6748  f0  6749  fconst  6754  f1ssr  6772  fof  6782  dff1o2  6816  dff2  7084  dff3  7085  fmpt  7095  ffnfv  7104  ffvresb  7111  idref  7132  fpr  7141  dff1o6  7263  fliftf  7303  fiun  7928  f1iun  7929  ffoss  7931  1stcof  8004  2ndcof  8005  smores  8327  smores2  8329  iordsmo  8332  sbthlem9  9071  inf3lem6  9590  alephsmo  10074  alephsing  10248  axdc3lem2  10423  smobeth  10559  fpwwe2lem10  10613  gruiun  10772  gruima  10775  nqerf  10903  om2uzf1oi  13980  fclim  15594  invf  17815  funcres2b  17944  funcres2c  17950  hofcllem  18304  hofcl  18305  nfchnd  18657  gsumval2  18734  resmgmhm2b  18761  resmhm2b  18871  frmdss2  18912  gsumval3a  19964  subgdmdprd  20097  srgfcl  20269  lsslindf  21940  indlcim  21950  cnrest2  23404  lmss  23416  conncn  23544  txflf  24124  cnextf  24184  clsnsg  24228  tgpconncomp  24231  psmetxrge0  24431  causs  25418  ellimc2  25997  perfdvf  26023  c1lip2  26118  dvne0  26131  plyeq0  26329  plyreres  26405  aannenlem1  26450  taylf  26482  ulmss  26518  elno2  27776  elno3  27777  cutsf  27943  madef  27987  oniso  28422  mpteleeOLD  29154  ausgrusgrb  29424  ausgrumgri  29426  usgrexmplef  29518  subuhgr  29545  subupgr  29546  subumgr  29547  subusgr  29548  upgrres  29565  umgrres  29566  hhssnv  31525  pjfi  31965  maprnin  32988  cycpmconjslem1  33387  esplyfv1  33876  measdivcstALTV  34532  sitgf  34654  eulerpartlemn  34688  reprinrn  34922  cvmlift2lem9a  35666  satff  35773  icoreresf  37858  poimirlem30  38161  poimirlem31  38162  isbnd3  38295  dihf11lem  41902  ofoafg  43943  ofoaid1  43947  ofoaid2  43948  naddcnff  43951  ntrf  44711  clsf2  44714  gneispace3  44721  gneispacef2  44724  k0004lem1  44735  dvsid  44905  stoweidlem27  46599  stoweidlem29  46601  stoweidlem31  46603  fourierdlem15  46694  mbfresmf  47311  sinnpoly  47483  ffnafv  47763  fcdmvafv2v  47828  iccpartf  48035  slotresfo  49528