Theorem endom 8918

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

Syntax hints:   → wi 4   class class class wbr 5098   ≈ cen 8882   ≼ cdom 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-br 5099  df-opab 5161  df-f1o 6499  df-en 8886  df-dom 8887

This theorem is referenced by:  bren2  8922  domrefg  8926  endomtr  8951  domentr  8952  domunsncan  9007  sbthb  9028  dom0  9035  sdomentr  9041  ensdomtr  9043  domtriord  9053  domunsn  9057  xpen  9070  sdomdomtrfi  9127  domsdomtrfi  9128  sucdom2  9129  php  9133  php3  9135  onomeneq  9140  0sdom1dom  9148  rex2dom  9155  unxpdom2  9162  sucxpdom  9163  f1finf1o  9175  findcard3  9185  fodomfi  9214  wdomen1  9483  wdomen2  9484  fidomtri2  9908  prdom2  9918  acnen  9965  acnen2  9967  alephdom  9993  alephinit  10007  undjudom  10080  pwdjudom  10127  fin1a2lem11  10322  hsmexlem1  10338  gchdomtri  10542  gchdjuidm  10581  gchxpidm  10582  gchpwdom  10583  gchhar  10592  gruina  10731  nnct  13906  odinf  19494  hauspwdom  23447  ufildom1  23872  iscmet3  25251  mbfaddlem  25619  ctbssinf  37613  pibt2  37624  heiborlem3  38016  zct  45327  qct  45628  caratheodory  46793