Theorem endom 8991

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

Syntax hints:   → wi 4   class class class wbr 5119   ≈ cen 8954   ≼ cdom 8955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-f1o 6537  df-en 8958  df-dom 8959

This theorem is referenced by:  bren2  8995  domrefg  8999  endomtr  9024  domentr  9025  domunsncan  9084  sbthb  9106  dom0  9114  sdomentr  9123  ensdomtr  9125  domtriord  9135  domunsn  9139  xpen  9152  sdomdomtrfi  9213  domsdomtrfi  9214  sucdom2  9215  php  9219  php3  9221  onomeneq  9235  0sdom1dom  9244  rex2dom  9252  unxpdom2  9260  sucxpdom  9261  f1finf1o  9275  findcard3  9288  fodomfi  9320  wdomen1  9588  wdomen2  9589  fidomtri2  10006  prdom2  10018  acnen  10065  acnen2  10067  alephdom  10093  alephinit  10107  undjudom  10180  pwdjudom  10227  fin1a2lem11  10422  hsmexlem1  10438  gchdomtri  10641  gchdjuidm  10680  gchxpidm  10681  gchpwdom  10682  gchhar  10691  gruina  10830  nnct  13997  odinf  19542  hauspwdom  23437  ufildom1  23862  iscmet3  25243  mbfaddlem  25611  ctbssinf  37370  pibt2  37381  heiborlem3  37783  zct  45033  qct  45337  caratheodory  46505