Theorem endom 9039

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

Syntax hints:   → wi 4   class class class wbr 5166   ≈ cen 9000   ≼ cdom 9001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-f1o 6580  df-en 9004  df-dom 9005

This theorem is referenced by:  bren2  9043  domrefg  9047  endomtr  9072  domentr  9073  domunsncan  9138  sbthb  9160  dom0  9168  sdomentr  9177  ensdomtr  9179  domtriord  9189  domunsn  9193  xpen  9206  sdomdomtrfi  9267  domsdomtrfi  9268  sucdom2  9269  php  9273  php3  9275  onomeneq  9291  0sdom1dom  9301  rex2dom  9309  unxpdom2  9317  sucxpdom  9318  f1finf1o  9333  findcard3  9346  fodomfi  9378  wdomen1  9645  wdomen2  9646  fidomtri2  10063  prdom2  10075  acnen  10122  acnen2  10124  alephdom  10150  alephinit  10164  undjudom  10237  pwdjudom  10284  fin1a2lem11  10479  hsmexlem1  10495  gchdomtri  10698  gchdjuidm  10737  gchxpidm  10738  gchpwdom  10739  gchhar  10748  gruina  10887  nnct  14032  odinf  19605  hauspwdom  23530  ufildom1  23955  iscmet3  25346  mbfaddlem  25714  ctbssinf  37372  pibt2  37383  heiborlem3  37773  zct  44963  qct  45277  caratheodory  46449