Metamath Proof Explorer


Theorem enen1

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

Ref Expression
Assertion enen1 ABACBC

Proof

Step Hyp Ref Expression
1 ensym ABBA
2 entr BAACBC
3 1 2 sylan ABACBC
4 entr ABBCAC
5 3 4 impbida ABACBC