Theorem endom 8953

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

Syntax hints:   → wi 4   class class class wbr 5110   ≈ cen 8918   ≼ cdom 8919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-f1o 6521  df-en 8922  df-dom 8923

This theorem is referenced by:  bren2  8957  domrefg  8961  endomtr  8986  domentr  8987  domunsncan  9046  sbthb  9068  dom0  9075  sdomentr  9081  ensdomtr  9083  domtriord  9093  domunsn  9097  xpen  9110  sdomdomtrfi  9171  domsdomtrfi  9172  sucdom2  9173  php  9177  php3  9179  onomeneq  9184  0sdom1dom  9192  rex2dom  9200  unxpdom2  9208  sucxpdom  9209  f1finf1o  9223  findcard3  9236  fodomfi  9268  wdomen1  9536  wdomen2  9537  fidomtri2  9954  prdom2  9966  acnen  10013  acnen2  10015  alephdom  10041  alephinit  10055  undjudom  10128  pwdjudom  10175  fin1a2lem11  10370  hsmexlem1  10386  gchdomtri  10589  gchdjuidm  10628  gchxpidm  10629  gchpwdom  10630  gchhar  10639  gruina  10778  nnct  13953  odinf  19500  hauspwdom  23395  ufildom1  23820  iscmet3  25200  mbfaddlem  25568  ctbssinf  37401  pibt2  37412  heiborlem3  37814  zct  45062  qct  45365  caratheodory  46533