Theorem endom 8914

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

Syntax hints:   → wi 4   class class class wbr 5096   ≈ cen 8878   ≼ cdom 8879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-br 5097  df-opab 5159  df-f1o 6497  df-en 8882  df-dom 8883

This theorem is referenced by:  bren2  8918  domrefg  8922  endomtr  8947  domentr  8948  domunsncan  9003  sbthb  9024  dom0  9031  sdomentr  9037  ensdomtr  9039  domtriord  9049  domunsn  9053  xpen  9066  sdomdomtrfi  9123  domsdomtrfi  9124  sucdom2  9125  php  9129  php3  9131  onomeneq  9136  0sdom1dom  9144  rex2dom  9151  unxpdom2  9158  sucxpdom  9159  f1finf1o  9171  findcard3  9181  fodomfi  9210  wdomen1  9479  wdomen2  9480  fidomtri2  9904  prdom2  9914  acnen  9961  acnen2  9963  alephdom  9989  alephinit  10003  undjudom  10076  pwdjudom  10123  fin1a2lem11  10318  hsmexlem1  10334  gchdomtri  10538  gchdjuidm  10577  gchxpidm  10578  gchpwdom  10579  gchhar  10588  gruina  10727  nnct  13902  odinf  19490  hauspwdom  23443  ufildom1  23868  iscmet3  25247  mbfaddlem  25615  ctbssinf  37550  pibt2  37561  heiborlem3  37953  zct  45248  qct  45549  caratheodory  46714