Definition df-f 4829

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 4821	. 2 wff 𝐹:A⟶B
5	3, 1	wfn 4820	. . 3 wff 𝐹 Fn A
6	3	crn 4269	. . . 4 class ran 𝐹
7	6, 2	wss 2890	. . 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  4952  feq2  4953  feq3  4954  nff  4965  sbcfg  4967  ffn  4968  dffn2  4969  frn  4974  dffn3  4975  fss  4976  fco  4977  funssxp  4981  fun  4984  fnfco  4986  fssres  4987  fcoi2  4992  fintm  4996  fin  4997  f0  5001  fconst  5003  f1ssr  5019  fof  5027  dff1o2  5052  fun11iun  5068  ffoss  5079  dff2  5232  fmpt  5240  ffnfv  5244  ffvresb  5249  fpr  5266  fprg  5267  idref  5317  dff1o6  5337  fliftf  5360  1stcof  5709  2ndcof  5710  smores  5825  smores2  5827  iordsmo  5830