Metamath Proof Explorer


Theorem ensymi

Description: Symmetry of equinumerosity. Theorem 2 of Suppes p. 92. (Contributed by NM, 25-Sep-2004)

Ref Expression
Hypothesis ensymi.2 A B
Assertion ensymi B A

Proof

Step Hyp Ref Expression
1 ensymi.2 A B
2 ensym A B B A
3 1 2 ax-mp B A