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	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → dom 𝐹 ≈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		funeq	⊢ ( 𝑥 = 𝐹 → ( Fun 𝑥 ↔ Fun 𝐹 ) )
2		dmeq	⊢ ( 𝑥 = 𝐹 → dom 𝑥 = dom 𝐹 )
3		id	⊢ ( 𝑥 = 𝐹 → 𝑥 = 𝐹 )
4	2 3	breq12d	⊢ ( 𝑥 = 𝐹 → ( dom 𝑥 ≈ 𝑥 ↔ dom 𝐹 ≈ 𝐹 ) )
5	1 4	imbi12d	⊢ ( 𝑥 = 𝐹 → ( ( Fun 𝑥 → dom 𝑥 ≈ 𝑥 ) ↔ ( Fun 𝐹 → dom 𝐹 ≈ 𝐹 ) ) )
6		vex	⊢ 𝑥 ∈ V
7	6	fundmen	⊢ ( Fun 𝑥 → dom 𝑥 ≈ 𝑥 )
8	5 7	vtoclg	⊢ ( 𝐹 ∈ 𝑉 → ( Fun 𝐹 → dom 𝐹 ≈ 𝐹 ) )
9	8	imp	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → dom 𝐹 ≈ 𝐹 )