Theorem endom 9006

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

Syntax hints:   → wi 4   class class class wbr 5152   ≈ cen 8967   ≼ cdom 8968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5688  df-rel 5689  df-f1o 6560  df-en 8971  df-dom 8972

This theorem is referenced by:  bren2  9010  domrefg  9014  endomtr  9039  domentr  9040  domunsncan  9103  sbthb  9125  dom0  9133  sdomentr  9142  ensdomtr  9144  domtriord  9154  domunsn  9158  xpen  9171  sdomdomtrfi  9235  domsdomtrfi  9236  sucdom2  9237  php  9241  php3  9243  onomeneq  9259  0sdom1dom  9269  rex2dom  9277  unxpdom2  9285  sucxpdom  9286  f1finf1o  9302  findcard3  9316  wdomen1  9607  wdomen2  9608  fidomtri2  10025  prdom2  10037  acnen  10084  acnen2  10086  alephdom  10112  alephinit  10126  undjudom  10198  pwdjudom  10247  fin1a2lem11  10441  hsmexlem1  10457  gchdomtri  10660  gchdjuidm  10699  gchxpidm  10700  gchpwdom  10701  gchhar  10710  gruina  10849  nnct  13986  odinf  19525  hauspwdom  23425  ufildom1  23850  iscmet3  25241  mbfaddlem  25609  ctbssinf  36918  pibt2  36929  heiborlem3  37319  zct  44456  qct  44773  caratheodory  45945