Definition df-f 6419

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 6954, dff3 6955, and dff4 6956. (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 6411	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6410	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5580	. . . 4 class ran 𝐹
7	6, 2	wss 3884	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 399	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6562  feq2  6563  feq3  6564  nff  6577  sbcfg  6579  ffn  6581  dffn2  6583  frn  6588  dffn3  6594  ffrnb  6596  fss  6598  fcof  6604  fcoOLD  6606  funssxp  6610  fdmrn  6613  fun  6617  fnfco  6620  fssres  6621  fcoi2  6630  fint  6634  fin  6635  f0  6636  fconst  6641  f1ssr  6658  fof  6669  dff1o2  6702  dff2  6954  dff3  6955  fmpt  6963  ffnfv  6971  ffvresb  6977  idref  6997  fpr  7005  dff1o6  7125  fliftf  7163  fiun  7756  f1iun  7757  ffoss  7759  1stcof  7831  2ndcof  7832  smores  8131  smores2  8133  iordsmo  8136  sbthlem9  8808  inf3lem6  9296  alephsmo  9764  alephsing  9938  axdc3lem2  10113  smobeth  10248  fpwwe2lem10  10302  gruiun  10461  gruima  10464  nqerf  10592  om2uzf1oi  13576  fclim  15165  invf  17372  funcres2b  17503  funcres2c  17508  hofcllem  17867  hofcl  17868  gsumval2  18260  resmhm2b  18351  frmdss2  18392  gsumval3a  19394  subgdmdprd  19527  srgfcl  19641  lsslindf  20922  indlcim  20932  cnrest2  22320  lmss  22332  conncn  22460  txflf  23040  cnextf  23100  clsnsg  23144  tgpconncomp  23147  psmetxrge0  23349  causs  24342  ellimc2  24921  perfdvf  24947  c1lip2  25042  dvne0  25055  plyeq0  25252  plyreres  25323  aannenlem1  25368  taylf  25400  ulmss  25436  mptelee  27141  ausgrusgrb  27413  ausgrumgri  27415  usgrexmplef  27504  subuhgr  27531  subupgr  27532  subumgr  27533  subusgr  27534  upgrres  27551  umgrres  27552  hhssnv  29502  pjfi  29942  maprnin  30943  cycpmconjslem1  31298  measdivcstALTV  32068  sitgf  32189  eulerpartlemn  32223  reprinrn  32473  cvmlift2lem9a  33140  satff  33247  elno2  33759  elno3  33760  scutf  33908  madef  33942  icoreresf  35429  poimirlem30  35713  poimirlem31  35714  isbnd3  35848  dihf11lem  39186  ntrf  41595  clsf2  41598  gneispace3  41605  gneispacef2  41608  k0004lem1  41619  dvsid  41811  stoweidlem27  43431  stoweidlem29  43433  stoweidlem31  43435  fourierdlem15  43526  mbfresmf  44135  ffnafv  44523  frnvafv2v  44588  iccpartf  44744  resmgmhm2b  45215