Theorem endom 8024

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

Syntax hints:   → wi 4   class class class wbr 4685   ≈ cen 7994   ≼ cdom 7995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-f1o 5933  df-en 7998  df-dom 7999

This theorem is referenced by:  bren2  8028  domrefg  8032  endomtr  8055  domentr  8056  domunsncan  8101  sbthb  8122  sdomentr  8135  ensdomtr  8137  domtriord  8147  domunsn  8151  xpen  8164  unxpdom2  8209  sucxpdom  8210  wdomen1  8522  wdomen2  8523  fidomtri2  8858  prdom2  8867  acnen  8914  acnen2  8916  alephdom  8942  alephinit  8956  uncdadom  9031  pwcdadom  9076  fin1a2lem11  9270  hsmexlem1  9286  gchdomtri  9489  gchcdaidm  9528  gchxpidm  9529  gchpwdom  9530  gchhar  9539  gruina  9678  nnct  12820  odinf  18026  hauspwdom  21352  ufildom1  21777  iscmet3  23137  ovolctb2  23306  mbfaddlem  23472  heiborlem3  33742  zct  39543  qct  39891  caratheodory  41063