Definition df-f 4849

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	⊢ (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ran 𝐹 ⊆ B))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf 4841	. 2 wff 𝐹:A⟶B
5	3, 1	wfn 4840	. . 3 wff 𝐹 Fn A
6	3	crn 4289	. . . 4 class ran 𝐹
7	6, 2	wss 2911	. . 3 wff ran 𝐹 ⊆ B
8	5, 7	wa 97	. 2 wff (𝐹 Fn A ∧ ran 𝐹 ⊆ B)
9	4, 8	wb 98	1 wff (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ran 𝐹 ⊆ B))

This definition is referenced by:  feq1  4973  feq2  4974  feq3  4975  nff  4986  sbcfg  4988  ffn  4989  dffn2  4990  frn  4995  dffn3  4996  fss  4997  fco  4999  funssxp  5003  fun  5006  fnfco  5008  fssres  5009  fcoi2  5014  fintm  5018  fin  5019  f0  5023  fconst  5025  f1ssr  5041  fof  5049  dff1o2  5074  fun11iun  5090  ffoss  5101  dff2  5254  fmpt  5262  ffnfv  5266  ffvresb  5271  fpr  5288  fprg  5289  idref  5339  dff1o6  5359  fliftf  5382  1stcof  5732  2ndcof  5733  smores  5848  smores2  5850  iordsmo  5853  frec2uzf1od  8833