Theorem endom 8972

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

Syntax hints:   → wi 4   class class class wbr 5109   ≈ cen 8936   ≼ cdom 8937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-f1o 6543  df-en 8940  df-dom 8941

This theorem is referenced by:  bren2  8976  domrefg  8980  endomtr  9005  domentr  9006  domunsncan  9061  sbthb  9082  dom0  9089  sdomentr  9095  ensdomtr  9097  domtriord  9107  domunsn  9111  xpen  9124  sdomdomtrfi  9181  domsdomtrfi  9182  sucdom2  9183  php  9187  php3  9189  onomeneq  9194  0sdom1dom  9202  rex2dom  9209  unxpdom2  9216  sucxpdom  9217  f1finf1o  9229  findcard3  9239  fodomfi  9268  wdomen1  9534  wdomen2  9535  fidomtri2  9976  prdom2  9986  acnen  10033  acnen2  10035  alephdom  10061  alephinit  10075  undjudom  10147  pwdjudom  10194  fin1a2lem11  10389  hsmexlem1  10405  gchdomtri  10609  gchdjuidm  10648  gchxpidm  10649  gchpwdom  10650  gchhar  10659  gruina  10798  nnct  14013  odinf  19628  hauspwdom  23658  ufildom1  24083  iscmet3  25452  mbfaddlem  25819  ctbssinf  38072  pibt2  38083  heiborlem3  38484  zct  45801  qct  46098  caratheodory  47262