Definition df-f 4926

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 4918	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 4917	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4364	. . . 4 class ran 𝐹
7	6, 2	wss 2973	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 102	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 103	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  5050  feq2  5051  feq3  5052  nff  5063  sbcfg  5065  ffn  5066  dffn2  5067  frn  5072  dffn3  5073  fss  5074  fco  5076  funssxp  5080  fun  5083  fnfco  5085  fssres  5086  fcoi2  5091  fintm  5095  fin  5096  f0  5100  fconst  5102  f1ssr  5118  fof  5126  dff1o2  5151  fun11iun  5167  ffoss  5178  dff2  5332  fmpt  5340  ffnfv  5344  ffvresb  5349  fpr  5366  fprg  5367  idref  5417  dff1o6  5436  fliftf  5459  1stcof  5810  2ndcof  5811  smores  5930  smores2  5932  iordsmo  5935  frec2uzf1od  9408  fclim  10133