Theorem endom 8927

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

Syntax hints:   → wi 4   class class class wbr 5102   ≈ cen 8892   ≼ cdom 8893

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638  df-f1o 6506  df-en 8896  df-dom 8897

This theorem is referenced by:  bren2  8931  domrefg  8935  endomtr  8960  domentr  8961  domunsncan  9018  sbthb  9039  dom0  9046  sdomentr  9052  ensdomtr  9054  domtriord  9064  domunsn  9068  xpen  9081  sdomdomtrfi  9142  domsdomtrfi  9143  sucdom2  9144  php  9148  php3  9150  onomeneq  9155  0sdom1dom  9162  rex2dom  9169  unxpdom2  9177  sucxpdom  9178  f1finf1o  9192  findcard3  9205  fodomfi  9237  wdomen1  9505  wdomen2  9506  fidomtri2  9923  prdom2  9935  acnen  9982  acnen2  9984  alephdom  10010  alephinit  10024  undjudom  10097  pwdjudom  10144  fin1a2lem11  10339  hsmexlem1  10355  gchdomtri  10558  gchdjuidm  10597  gchxpidm  10598  gchpwdom  10599  gchhar  10608  gruina  10747  nnct  13922  odinf  19477  hauspwdom  23421  ufildom1  23846  iscmet3  25226  mbfaddlem  25594  ctbssinf  37387  pibt2  37398  heiborlem3  37800  zct  45048  qct  45351  caratheodory  46519