Metamath Proof Explorer

Theorem enrefg

Description: Equinumerosity is reflexive. Theorem 1 of Suppes p. 92. (Contributed by NM, 18-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion enrefg 
|- ( A e. V -> A ~~ A )

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` A ) : A -1-1-onto-> A
2 f1oen2g 
 |-  ( ( A e. V /\ A e. V /\ ( _I |` A ) : A -1-1-onto-> A ) -> A ~~ A )
3 1 2 mp3an3 
 |-  ( ( A e. V /\ A e. V ) -> A ~~ A )
4 3 anidms 
 |-  ( A e. V -> A ~~ A )