Metamath Proof Explorer


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 𝐹𝐹 )