Theorem endom 8904

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

Syntax hints:   → wi 4   class class class wbr 5092   ≈ cen 8869   ≼ cdom 8870

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626  df-f1o 6489  df-en 8873  df-dom 8874

This theorem is referenced by:  bren2  8908  domrefg  8912  endomtr  8937  domentr  8938  domunsncan  8994  sbthb  9015  dom0  9022  sdomentr  9028  ensdomtr  9030  domtriord  9040  domunsn  9044  xpen  9057  sdomdomtrfi  9115  domsdomtrfi  9116  sucdom2  9117  php  9121  php3  9123  onomeneq  9128  0sdom1dom  9135  rex2dom  9142  unxpdom2  9149  sucxpdom  9150  f1finf1o  9162  findcard3  9172  fodomfi  9201  wdomen1  9468  wdomen2  9469  fidomtri2  9890  prdom2  9900  acnen  9947  acnen2  9949  alephdom  9975  alephinit  9989  undjudom  10062  pwdjudom  10109  fin1a2lem11  10304  hsmexlem1  10320  gchdomtri  10523  gchdjuidm  10562  gchxpidm  10563  gchpwdom  10564  gchhar  10573  gruina  10712  nnct  13888  odinf  19442  hauspwdom  23386  ufildom1  23811  iscmet3  25191  mbfaddlem  25559  ctbssinf  37390  pibt2  37401  heiborlem3  37803  zct  45049  qct  45352  caratheodory  46519