Metamath Proof Explorer

Theorem domen1

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

Ref Expression
Assertion domen1 
|- ( A ~~ B -> ( A ~<_ C <-> B ~<_ C ) )

Proof

Step Hyp Ref Expression
1 ensym 
 |-  ( A ~~ B -> B ~~ A )
2 endomtr 
 |-  ( ( B ~~ A /\ A ~<_ C ) -> B ~<_ C )
3 1 2 sylan 
 |-  ( ( A ~~ B /\ A ~<_ C ) -> B ~<_ C )
4 endomtr 
 |-  ( ( A ~~ B /\ B ~<_ C ) -> A ~<_ C )
5 3 4 impbida 
 |-  ( A ~~ B -> ( A ~<_ C <-> B ~<_ C ) )