Theorem endom 8988

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-f1o 6540  df-en 8956  df-dom 8957

This theorem is used by:  bren2  8992  domrefg  8996  endomtr  9021  domentr  9022  domunsncan  9078  sbthb  9099  dom0  9106  sdomentr  9112  ensdomtr  9114  domtriord  9124  domunsn  9128  xpen  9141  sdomdomtrfi  9198  domsdomtrfi  9199  sucdom2  9200  php  9204  php3  9206  onomeneq  9211  0sdom1dom  9219  rex2dom  9226  unxpdom2  9233  sucxpdom  9234  f1finf1o  9246  findcard3  9256  fodomfi  9285  wdomen1  9551  wdomen2  9552  fidomtri2  10002  prdom2  10012  acnen  10059  acnen2  10061  alephdom  10087  alephinit  10101  undjudom  10173  pwdjudom  10220  fin1a2lem11  10415  hsmexlem1  10431  gchdomtri  10641  gchdjuidm  10680  gchxpidm  10681  gchpwdom  10682  gchhar  10691  gruina  10830  nnct  14048  odinf  19693  hauspwdom  23730  ufildom1  24155  iscmet3  25524  mbfaddlem  25891  ctbssinf  38163  pibt2  38174  heiborlem3  38566  zct  45898  qct  46195  caratheodory  47359