Definition df-f 5220

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (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 5212	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5211	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4627	. . . 4 class ran 𝐹
7	6, 2	wss 3129	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 104	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 105	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  5348  feq2  5349  feq3  5350  nff  5362  sbcfg  5364  ffn  5365  dffn2  5367  frn  5374  dffn3  5376  fss  5377  fco  5381  funssxp  5385  fun  5388  fnfco  5390  fssres  5391  fcoi2  5397  fintm  5401  fin  5402  f0  5406  fconst  5411  f1ssr  5428  fof  5438  dff1o2  5466  fun11iun  5482  ffoss  5493  dff2  5660  fmpt  5666  ffnfv  5674  ffvresb  5679  fpr  5698  fprg  5699  idref  5757  dff1o6  5776  fliftf  5799  1stcof  6163  2ndcof  6164  smores  6292  smores2  6294  iordsmo  6297  tfrcllembfn  6357  sbthlemi9  6963  inresflem  7058  frec2uzf1od  10403  frecuzrdgtcl  10409  fclim  11297  ennnfonelemf1  12413  srgfcl  13149  cnrest2  13667  lmss  13677  psmetxrge0  13763  dvfgg  14088  nninfall  14678