Metamath Proof Explorer

Theorem enref

Description: Equinumerosity is reflexive. Theorem 1 of Suppes p. 92. (Contributed by NM, 25-Sep-2004)

Ref Expression
Hypothesis enref.1 
|- A e. _V
Assertion enref 
|- A ~~ A

Proof

Step Hyp Ref Expression
1 enref.1 
 |-  A e. _V
2 enrefg 
 |-  ( A e. _V -> A ~~ A )
3 1 2 ax-mp 
 |-  A ~~ A