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 A B A B

Proof

Step Hyp Ref Expression
1 enssdom
2 1 ssbri A B A B