Theorem endom 8982

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

This proof depends on syntax axioms:   → wi 4   class class class wbr 5111   ≈ cen 8946   ≼ cdom 8947

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-f1o 6547  df-en 8950  df-dom 8951

This theorem is used by:  bren2  8986  domrefg  8990  endomtr  9015  domentr  9016  domunsncan  9072  sbthb  9093  dom0  9100  sdomentr  9106  ensdomtr  9108  domtriord  9118  domunsn  9122  xpen  9135  sdomdomtrfi  9192  domsdomtrfi  9193  sucdom2  9194  php  9198  php3  9200  onomeneq  9205  0sdom1dom  9213  rex2dom  9220  unxpdom2  9227  sucxpdom  9228  f1finf1o  9240  findcard3  9250  fodomfi  9279  wdomen1  9545  wdomen2  9546  fidomtri2  9996  prdom2  10006  acnen  10053  acnen2  10055  alephdom  10081  alephinit  10095  undjudom  10167  pwdjudom  10214  fin1a2lem11  10409  hsmexlem1  10425  gchdomtri  10631  gchdjuidm  10670  gchxpidm  10671  gchpwdom  10672  gchhar  10681  gruina  10820  nnct  14037  odinf  19679  hauspwdom  23711  ufildom1  24136  iscmet3  25505  mbfaddlem  25872  ctbssinf  38111  pibt2  38122  heiborlem3  38524  zct  45841  qct  46138  caratheodory  47302