Theorem endom 9017

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

Syntax hints:   → wi 4   class class class wbr 5147   ≈ cen 8980   ≼ cdom 8981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-f1o 6569  df-en 8984  df-dom 8985

This theorem is referenced by:  bren2  9021  domrefg  9025  endomtr  9050  domentr  9051  domunsncan  9110  sbthb  9132  dom0  9140  sdomentr  9149  ensdomtr  9151  domtriord  9161  domunsn  9165  xpen  9178  sdomdomtrfi  9238  domsdomtrfi  9239  sucdom2  9240  php  9244  php3  9246  onomeneq  9262  0sdom1dom  9271  rex2dom  9279  unxpdom2  9287  sucxpdom  9288  f1finf1o  9302  findcard3  9315  fodomfi  9347  wdomen1  9613  wdomen2  9614  fidomtri2  10031  prdom2  10043  acnen  10090  acnen2  10092  alephdom  10118  alephinit  10132  undjudom  10205  pwdjudom  10252  fin1a2lem11  10447  hsmexlem1  10463  gchdomtri  10666  gchdjuidm  10705  gchxpidm  10706  gchpwdom  10707  gchhar  10716  gruina  10855  nnct  14018  odinf  19595  hauspwdom  23524  ufildom1  23949  iscmet3  25340  mbfaddlem  25708  ctbssinf  37388  pibt2  37399  heiborlem3  37799  zct  45000  qct  45311  caratheodory  46483