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 ⊢ ≈ ⊆ ≼
2 1 ssbri ⊢ A ≈ B → A ≼ B