Theorem endom 8926

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

Syntax hints:   → wi 4   class class class wbr 5085   ≈ cen 8890   ≼ cdom 8891

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-f1o 6505  df-en 8894  df-dom 8895

This theorem is referenced by:  bren2  8930  domrefg  8934  endomtr  8959  domentr  8960  domunsncan  9015  sbthb  9036  dom0  9043  sdomentr  9049  ensdomtr  9051  domtriord  9061  domunsn  9065  xpen  9078  sdomdomtrfi  9135  domsdomtrfi  9136  sucdom2  9137  php  9141  php3  9143  onomeneq  9148  0sdom1dom  9156  rex2dom  9163  unxpdom2  9170  sucxpdom  9171  f1finf1o  9183  findcard3  9193  fodomfi  9222  wdomen1  9491  wdomen2  9492  fidomtri2  9918  prdom2  9928  acnen  9975  acnen2  9977  alephdom  10003  alephinit  10017  undjudom  10090  pwdjudom  10137  fin1a2lem11  10332  hsmexlem1  10348  gchdomtri  10552  gchdjuidm  10591  gchxpidm  10592  gchpwdom  10593  gchhar  10602  gruina  10741  nnct  13943  odinf  19538  hauspwdom  23466  ufildom1  23891  iscmet3  25260  mbfaddlem  25627  ctbssinf  37722  pibt2  37733  heiborlem3  38134  zct  45492  qct  45792  caratheodory  46956