Metamath Proof Explorer


Theorem sdomen2

Description: Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003)

Ref Expression
Assertion sdomen2 ABCACB

Proof

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