Definition df-f 4821

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 4813	. 2 wff 𝐹:A⟶B
5	3, 1	wfn 4812	. . 3 wff 𝐹 Fn A
6	3	crn 4261	. . . 4 class ran 𝐹
7	6, 2	wss 2885	. . 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  4944  feq2  4945  feq3  4946  nff  4957  sbcfg  4959  ffn  4960  dffn2  4961  frn  4966  dffn3  4967  fss  4968  fco  4969  funssxp  4973  fun  4976  fnfco  4978  fssres  4979  fcoi2  4984  fintm  4988  fin  4989  f0  4993  fconst  4995  f1ssr  5011  fof  5019  dff1o2  5044  fun11iun  5060  ffoss  5071  dff2  5224  fmpt  5232  ffnfv  5236  ffvresb  5241  fpr  5258  fprg  5259  idref  5309  dff1o6  5329  fliftf  5352  1stcof  5701  2ndcof  5702  smores  5817  smores2  5819  iordsmo  5822