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 
|- ( ( F e. V /\ Fun F ) -> dom F ~~ F )

Proof

Step Hyp Ref Expression
1 funeq 
 |-  ( x = F -> ( Fun x <-> Fun F ) )
2 dmeq 
 |-  ( x = F -> dom x = dom F )
3 id 
 |-  ( x = F -> x = F )
4 2 3 breq12d 
 |-  ( x = F -> ( dom x ~~ x <-> dom F ~~ F ) )
5 1 4 imbi12d 
 |-  ( x = F -> ( ( Fun x -> dom x ~~ x ) <-> ( Fun F -> dom F ~~ F ) ) )
6 vex 
 |-  x e. _V
7 6 fundmen 
 |-  ( Fun x -> dom x ~~ x )
8 5 7 vtoclg 
 |-  ( F e. V -> ( Fun F -> dom F ~~ F ) )
9 8 imp 
 |-  ( ( F e. V /\ Fun F ) -> dom F ~~ F )