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 V
Assertion enref A A

Proof

Step Hyp Ref Expression
1 enref.1 A V
2 enrefg A V A A
3 1 2 ax-mp A A