Theorem endom 8928

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

Syntax hints:   → wi 4   class class class wbr 5100   ≈ cen 8892   ≼ cdom 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-f1o 6507  df-en 8896  df-dom 8897

This theorem is referenced by:  bren2  8932  domrefg  8936  endomtr  8961  domentr  8962  domunsncan  9017  sbthb  9038  dom0  9045  sdomentr  9051  ensdomtr  9053  domtriord  9063  domunsn  9067  xpen  9080  sdomdomtrfi  9137  domsdomtrfi  9138  sucdom2  9139  php  9143  php3  9145  onomeneq  9150  0sdom1dom  9158  rex2dom  9165  unxpdom2  9172  sucxpdom  9173  f1finf1o  9185  findcard3  9195  fodomfi  9224  wdomen1  9493  wdomen2  9494  fidomtri2  9918  prdom2  9928  acnen  9975  acnen2  9977  alephdom  10003  alephinit  10017  undjudom  10090  pwdjudom  10137  fin1a2lem11  10332  hsmexlem1  10348  gchdomtri  10552  gchdjuidm  10591  gchxpidm  10592  gchpwdom  10593  gchhar  10602  gruina  10741  nnct  13916  odinf  19507  hauspwdom  23460  ufildom1  23885  iscmet3  25264  mbfaddlem  25632  ctbssinf  37665  pibt2  37676  heiborlem3  38068  zct  45425  qct  45725  caratheodory  46890