Theorem endom 8901

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

Syntax hints:   → wi 4   class class class wbr 5089   ≈ cen 8866   ≼ cdom 8867

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 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-xp 5620  df-rel 5621  df-f1o 6488  df-en 8870  df-dom 8871

This theorem is referenced by:  bren2  8905  domrefg  8909  endomtr  8934  domentr  8935  domunsncan  8990  sbthb  9011  dom0  9018  sdomentr  9024  ensdomtr  9026  domtriord  9036  domunsn  9040  xpen  9053  sdomdomtrfi  9110  domsdomtrfi  9111  sucdom2  9112  php  9116  php3  9118  onomeneq  9123  0sdom1dom  9130  rex2dom  9137  unxpdom2  9144  sucxpdom  9145  f1finf1o  9157  findcard3  9167  fodomfi  9196  wdomen1  9462  wdomen2  9463  fidomtri2  9887  prdom2  9897  acnen  9944  acnen2  9946  alephdom  9972  alephinit  9986  undjudom  10059  pwdjudom  10106  fin1a2lem11  10301  hsmexlem1  10317  gchdomtri  10520  gchdjuidm  10559  gchxpidm  10560  gchpwdom  10561  gchhar  10570  gruina  10709  nnct  13888  odinf  19475  hauspwdom  23416  ufildom1  23841  iscmet3  25220  mbfaddlem  25588  ctbssinf  37450  pibt2  37461  heiborlem3  37863  zct  45168  qct  45471  caratheodory  46636