Theorem endom 8920

Description: Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)

Assertion

Ref	Expression
endom	⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)

Proof of Theorem endom

Step	Hyp	Ref	Expression
1		enssdom 8917	. 2 ⊢ ≈ ⊆ ≼
2	1	ssbri 5131	1 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)

Syntax hints:   → wi 4   class class class wbr 5086   ≈ cen 8884   ≼ cdom 8885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-f1o 6500  df-en 8888  df-dom 8889

This theorem is referenced by:  bren2  8924  domrefg  8928  endomtr  8953  domentr  8954  domunsncan  9009  sbthb  9030  dom0  9037  sdomentr  9043  ensdomtr  9045  domtriord  9055  domunsn  9059  xpen  9072  sdomdomtrfi  9129  domsdomtrfi  9130  sucdom2  9131  php  9135  php3  9137  onomeneq  9142  0sdom1dom  9150  rex2dom  9157  unxpdom2  9164  sucxpdom  9165  f1finf1o  9177  findcard3  9187  fodomfi  9216  wdomen1  9485  wdomen2  9486  fidomtri2  9912  prdom2  9922  acnen  9969  acnen2  9971  alephdom  9997  alephinit  10011  undjudom  10084  pwdjudom  10131  fin1a2lem11  10326  hsmexlem1  10342  gchdomtri  10546  gchdjuidm  10585  gchxpidm  10586  gchpwdom  10587  gchhar  10596  gruina  10735  nnct  13937  odinf  19532  hauspwdom  23479  ufildom1  23904  iscmet3  25273  mbfaddlem  25640  ctbssinf  37739  pibt2  37750  heiborlem3  38151  zct  45513  qct  45813  caratheodory  46977