Metamath Proof Explorer


Theorem enen2

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

Ref Expression
Assertion enen2 A B C A C B

Proof

Step Hyp Ref Expression
1 entr C A A B C B
2 1 ancoms A B C A C B
3 ensym A B B A
4 entr C B B A C A
5 4 ancoms B A C B C A
6 3 5 sylan A B C B C A
7 2 6 impbida A B C A C B