Theorem endom 9006

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

This proof depends on syntax axioms:   → wi 4   class class class wbr 5103   ≈ cen 8970   ≼ cdom 8971

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-f1o 6545  df-en 8974  df-dom 8975

This theorem is used by:  bren2  9010  domrefg  9014  endomtr  9039  domentr  9040  domunsncan  9096  sbthb  9117  dom0  9124  sdomentr  9130  ensdomtr  9132  domtriord  9142  domunsn  9146  xpen  9159  sdomdomtrfi  9216  domsdomtrfi  9217  sucdom2  9218  php  9222  php3  9224  onomeneq  9229  0sdom1dom  9237  rex2dom  9244  unxpdom2  9251  sucxpdom  9252  f1finf1o  9264  findcard3  9274  fodomfi  9304  wdomen1  9570  wdomen2  9571  fidomtri2  10075  prdom2  10085  acnen  10132  acnen2  10134  alephdom  10160  alephinit  10174  undjudom  10246  pwdjudom  10293  fin1a2lem11  10488  hsmexlem1  10504  gchdomtri  10714  gchdjuidm  10753  gchxpidm  10754  gchpwdom  10755  gchhar  10764  gruina  10903  nnct  14124  odinf  19777  hauspwdom  23820  ufildom1  24245  iscmet3  25614  mbfaddlem  25981  ctbssinf  38329  pibt2  38340  heiborlem3  38747  zct  46077  qct  46373  caratheodory  47537