Theorem endom 8926

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

Syntax hints:   → wi 4   class class class wbr 5110   ≈ cen 8887   ≼ cdom 8888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-rel 5645  df-f1o 6508  df-en 8891  df-dom 8892

This theorem is referenced by:  bren2  8930  domrefg  8934  endomtr  8959  domentr  8960  domunsncan  9023  sbthb  9045  dom0  9053  sdomentr  9062  ensdomtr  9064  domtriord  9074  domunsn  9078  xpen  9091  sdomdomtrfi  9155  domsdomtrfi  9156  sucdom2  9157  php  9161  php3  9163  onomeneq  9179  0sdom1dom  9189  rex2dom  9197  unxpdom2  9205  sucxpdom  9206  f1finf1o  9222  findcard3  9236  wdomen1  9521  wdomen2  9522  fidomtri2  9939  prdom2  9951  acnen  9998  acnen2  10000  alephdom  10026  alephinit  10040  undjudom  10112  pwdjudom  10161  fin1a2lem11  10355  hsmexlem1  10371  gchdomtri  10574  gchdjuidm  10613  gchxpidm  10614  gchpwdom  10615  gchhar  10624  gruina  10763  nnct  13896  odinf  19359  hauspwdom  22889  ufildom1  23314  iscmet3  24694  mbfaddlem  25061  ctbssinf  35950  pibt2  35961  heiborlem3  36345  zct  43391  qct  43717  caratheodory  44889