Theorem sdomnen

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

	Ref	Expression
Assertion	sdomnen	$$⊢A\prec B\to \neg A\approx B$$

Proof

Step	Hyp	Ref	Expression
1		brsdom	$$⊢A\prec B\leftrightarrow \left(A\preccurlyeq B\wedge \neg A\approx B\right)$$
2	1	simprbi	$$⊢A\prec B\to \neg A\approx B$$