Metamath Proof Explorer


Theorem sdomnen

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

Ref Expression
Assertion sdomnen A B ¬ A B

Proof

Step Hyp Ref Expression
1 brsdom A B A B ¬ A B
2 1 simprbi A B ¬ A B