Definition df-fn

Description: Define a function with domain. Definition 6.15(1) of TakeutiZaring p. 27. For alternate definitions, see dffn2 , dffn3 , dffn4 , and dffn5 . (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Assertion	df-fn	$$⊢AFnB\leftrightarrow \left(\mathrm{Fun}A\wedge \mathrm{dom}A=B\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	wfn	$$wffAFnB$$
3	0	wfun	$$wff\mathrm{Fun}A$$
4	0	cdm	$$class\mathrm{dom}A$$
5	4 1	wceq	$$wff\mathrm{dom}A=B$$
6	3 5	wa	$$wff\left(\mathrm{Fun}A\wedge \mathrm{dom}A=B\right)$$
7	2 6	wb	$$wff\left(AFnB\leftrightarrow \left(\mathrm{Fun}A\wedge \mathrm{dom}A=B\right)\right)$$