Theorem endom 9020

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

This proof depends on syntax axioms:   → wi 4   class class class wbr 5106   ≈ cen 8984   ≼ cdom 8985

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5107  df-opab 5171  df-f1o 6554  df-en 8988  df-dom 8989

This theorem is used by:  bren2  9024  domrefg  9028  endomtr  9053  domentr  9054  domunsncan  9110  sbthb  9131  dom0  9138  sdomentr  9144  ensdomtr  9146  domtriord  9156  domunsn  9160  xpen  9173  sdomdomtrfi  9230  domsdomtrfi  9231  sucdom2  9232  php  9236  php3  9238  onomeneq  9243  0sdom1dom  9251  rex2dom  9258  unxpdom2  9265  sucxpdom  9266  f1finf1o  9278  findcard3  9288  fodomfi  9318  wdomen1  9583  wdomen2  9584  fidomtri2  10088  prdom2  10098  acnen  10145  acnen2  10147  alephdom  10173  alephinit  10187  undjudom  10259  pwdjudom  10306  fin1a2lem11  10501  hsmexlem1  10517  gchdomtri  10727  gchdjuidm  10766  gchxpidm  10767  gchpwdom  10768  gchhar  10777  gruina  10916  nnct  14137  odinf  19792  hauspwdom  23835  ufildom1  24260  iscmet3  25629  mbfaddlem  25996  ctbssinf  38472  pibt2  38483  heiborlem3  38890  zct  46220  qct  46516  caratheodory  47680