Theorem fundmeng

Description: A function is equinumerous to its domain. Exercise 4 of Suppes p. 98. (Contributed by NM, 17-Sep-2013)

	Ref	Expression
Assertion	fundmeng	$$⊢\left(F\in V\wedge \mathrm{Fun}F\right)\to \mathrm{dom}F\approx F$$

Proof

Step	Hyp	Ref	Expression
1		funeq	$$⊢x=F\to \left(\mathrm{Fun}x\leftrightarrow \mathrm{Fun}F\right)$$
2		dmeq	$$⊢x=F\to \mathrm{dom}x=\mathrm{dom}F$$
3		id	$$⊢x=F\to x=F$$
4	2 3	breq12d	$$⊢x=F\to \left(\mathrm{dom}x\approx x\leftrightarrow \mathrm{dom}F\approx F\right)$$
5	1 4	imbi12d	$$⊢x=F\to \left(\left(\mathrm{Fun}x\to \mathrm{dom}x\approx x\right)\leftrightarrow \left(\mathrm{Fun}F\to \mathrm{dom}F\approx F\right)\right)$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6	fundmen	$$⊢\mathrm{Fun}x\to \mathrm{dom}x\approx x$$
8	5 7	vtoclg	$$⊢F\in V\to \left(\mathrm{Fun}F\to \mathrm{dom}F\approx F\right)$$
9	8	imp	$$⊢\left(F\in V\wedge \mathrm{Fun}F\right)\to \mathrm{dom}F\approx F$$