Theorem endom 8917

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 8914	. 2 ⊢ ≈ ⊆ ≼
2	1	ssbri 5118	1 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)

Syntax hints:   → wi 4   class class class wbr 5073   ≈ cen 8881   ≼ cdom 8882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5074  df-opab 5136  df-f1o 6493  df-en 8885  df-dom 8886

This theorem is referenced by:  bren2  8921  domrefg  8925  endomtr  8950  domentr  8951  domunsncan  9006  sbthb  9027  dom0  9034  sdomentr  9040  ensdomtr  9042  domtriord  9052  domunsn  9056  xpen  9069  sdomdomtrfi  9126  domsdomtrfi  9127  sucdom2  9128  php  9132  php3  9134  onomeneq  9139  0sdom1dom  9147  rex2dom  9154  unxpdom2  9161  sucxpdom  9162  f1finf1o  9174  findcard3  9184  fodomfi  9213  wdomen1  9482  wdomen2  9483  fidomtri2  9910  prdom2  9920  acnen  9967  acnen2  9969  alephdom  9995  alephinit  10009  undjudom  10082  pwdjudom  10129  fin1a2lem11  10324  hsmexlem1  10340  gchdomtri  10544  gchdjuidm  10583  gchxpidm  10584  gchpwdom  10585  gchhar  10594  gruina  10733  nnct  13935  odinf  19530  hauspwdom  23485  ufildom1  23910  iscmet3  25279  mbfaddlem  25646  ctbssinf  37777  pibt2  37788  heiborlem3  38189  zct  45518  qct  45815  caratheodory  46979