This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵 )

Proof

Step Hyp Ref Expression
1 enssdom ⊢ ≈ ⊆ ≼
2 1 ssbri ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵 )