Metamath Proof Explorer

Theorem endom

Description: Equinumerosity implies dominance. Theorem 15 of Suppes p. 94. (Contributed by NM, 28-May-1998)

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

Proof

Step Hyp Ref Expression
1 enssdom 
 |-  ~~ C_ ~<_
2 1 ssbri 
 |-  ( A ~~ B -> A ~<_ B )