Theorem endom 8976

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

Syntax hints:   → wi 4   class class class wbr 5113   ≈ cen 8940   ≼ cdom 8941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5114  df-opab 5178  df-f1o 6544  df-en 8944  df-dom 8945

This theorem is referenced by:  bren2  8980  domrefg  8984  endomtr  9009  domentr  9010  domunsncan  9065  sbthb  9086  dom0  9093  sdomentr  9099  ensdomtr  9101  domtriord  9111  domunsn  9115  xpen  9128  sdomdomtrfi  9185  domsdomtrfi  9186  sucdom2  9187  php  9191  php3  9193  onomeneq  9198  0sdom1dom  9206  rex2dom  9213  unxpdom2  9220  sucxpdom  9221  f1finf1o  9233  findcard3  9243  fodomfi  9272  wdomen1  9538  wdomen2  9539  fidomtri2  9980  prdom2  9990  acnen  10037  acnen2  10039  alephdom  10065  alephinit  10079  undjudom  10151  pwdjudom  10198  fin1a2lem11  10394  hsmexlem1  10410  gchdomtri  10614  gchdjuidm  10653  gchxpidm  10654  gchpwdom  10655  gchhar  10664  gruina  10803  nnct  14017  odinf  19633  hauspwdom  23627  ufildom1  24052  iscmet3  25421  mbfaddlem  25788  ctbssinf  37974  pibt2  37985  heiborlem3  38386  zct  45707  qct  46004  caratheodory  47168