Theorem endom 8950

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

Syntax hints:   → wi 4   class class class wbr 5107   ≈ cen 8915   ≼ cdom 8916

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-f1o 6518  df-en 8919  df-dom 8920

This theorem is referenced by:  bren2  8954  domrefg  8958  endomtr  8983  domentr  8984  domunsncan  9041  sbthb  9062  dom0  9069  sdomentr  9075  ensdomtr  9077  domtriord  9087  domunsn  9091  xpen  9104  sdomdomtrfi  9165  domsdomtrfi  9166  sucdom2  9167  php  9171  php3  9173  onomeneq  9178  0sdom1dom  9185  rex2dom  9193  unxpdom2  9201  sucxpdom  9202  f1finf1o  9216  findcard3  9229  fodomfi  9261  wdomen1  9529  wdomen2  9530  fidomtri2  9947  prdom2  9959  acnen  10006  acnen2  10008  alephdom  10034  alephinit  10048  undjudom  10121  pwdjudom  10168  fin1a2lem11  10363  hsmexlem1  10379  gchdomtri  10582  gchdjuidm  10621  gchxpidm  10622  gchpwdom  10623  gchhar  10632  gruina  10771  nnct  13946  odinf  19493  hauspwdom  23388  ufildom1  23813  iscmet3  25193  mbfaddlem  25561  ctbssinf  37394  pibt2  37405  heiborlem3  37807  zct  45055  qct  45358  caratheodory  46526