Theorem ensymi

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

	Ref	Expression
Hypothesis	ensymi.2	⊢ 𝐴 ≈ 𝐵
Assertion	ensymi	⊢ 𝐵 ≈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		ensymi.2	⊢ 𝐴 ≈ 𝐵
2		ensym	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
3	1 2	ax-mp	⊢ 𝐵 ≈ 𝐴