Metamath Proof Explorer


Theorem enen2

Description: Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003)

Ref Expression
Assertion enen2 ABCACB

Proof

Step Hyp Ref Expression
1 entr CAABCB
2 1 ancoms ABCACB
3 ensym ABBA
4 entr CBBACA
5 4 ancoms BACBCA
6 3 5 sylan ABCBCA
7 2 6 impbida ABCACB