Definition df-f 4906

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 4898	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 4897	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4346	. . . 4 class ran 𝐹
7	6, 2	wss 2917	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 97	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 98	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  5030  feq2  5031  feq3  5032  nff  5043  sbcfg  5045  ffn  5046  dffn2  5047  frn  5052  dffn3  5053  fss  5054  fco  5056  funssxp  5060  fun  5063  fnfco  5065  fssres  5066  fcoi2  5071  fintm  5075  fin  5076  f0  5080  fconst  5082  f1ssr  5098  fof  5106  dff1o2  5131  fun11iun  5147  ffoss  5158  dff2  5311  fmpt  5319  ffnfv  5323  ffvresb  5328  fpr  5345  fprg  5346  idref  5396  dff1o6  5416  fliftf  5439  1stcof  5790  2ndcof  5791  smores  5907  smores2  5909  iordsmo  5912  frec2uzf1od  9192  fclim  9815