Theorem endom 8961

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

Syntax hints:   → wi 4   class class class wbr 5101   ≈ cen 8925   ≼ cdom 8926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5102  df-opab 5164  df-f1o 6529  df-en 8929  df-dom 8930

This theorem is referenced by:  bren2  8965  domrefg  8969  endomtr  8994  domentr  8995  domunsncan  9050  sbthb  9071  dom0  9078  sdomentr  9084  ensdomtr  9086  domtriord  9096  domunsn  9100  xpen  9113  sdomdomtrfi  9170  domsdomtrfi  9171  sucdom2  9172  php  9176  php3  9178  onomeneq  9183  0sdom1dom  9191  rex2dom  9198  unxpdom2  9205  sucxpdom  9206  f1finf1o  9218  findcard3  9228  fodomfi  9257  wdomen1  9525  wdomen2  9526  fidomtri2  9953  prdom2  9963  acnen  10010  acnen2  10012  alephdom  10038  alephinit  10052  undjudom  10125  pwdjudom  10172  fin1a2lem11  10368  hsmexlem1  10384  gchdomtri  10588  gchdjuidm  10627  gchxpidm  10628  gchpwdom  10629  gchhar  10638  gruina  10777  nnct  13995  odinf  19604  hauspwdom  23562  ufildom1  23987  iscmet3  25356  mbfaddlem  25723  ctbssinf  37901  pibt2  37912  heiborlem3  38313  zct  45642  qct  45939  caratheodory  47103