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