Theorem endom 8759

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

Syntax hints:   → wi 4   class class class wbr 5079   ≈ cen 8722   ≼ cdom 8723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-xp 5596  df-rel 5597  df-f1o 6439  df-en 8726  df-dom 8727

This theorem is referenced by:  bren2  8763  domrefg  8767  endomtr  8790  domentr  8791  domunsncan  8850  sbthb  8872  dom0  8880  sdomentr  8889  ensdomtr  8891  domtriord  8901  domunsn  8905  xpen  8918  sdomdomtrfi  8978  domsdomtrfi  8979  php  8983  php3  8985  unxpdom2  9019  sucxpdom  9020  wdomen1  9323  wdomen2  9324  fidomtri2  9763  prdom2  9773  acnen  9820  acnen2  9822  alephdom  9848  alephinit  9862  undjudom  9934  pwdjudom  9983  fin1a2lem11  10177  hsmexlem1  10193  gchdomtri  10396  gchdjuidm  10435  gchxpidm  10436  gchpwdom  10437  gchhar  10446  gruina  10585  nnct  13712  odinf  19181  hauspwdom  22663  ufildom1  23088  iscmet3  24468  mbfaddlem  24835  ctbssinf  35586  pibt2  35597  heiborlem3  35980  zct  42591  qct  42883  caratheodory  44048