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	⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )