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

Metamath Proof Explorer

Theorem sdomnen

Description: Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998)

Ref Expression
Assertion sdomnen ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )

Proof

Step Hyp Ref Expression
1 brsdom ⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) )
2 1 simprbi ⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )