Theorem endom 9019

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 5188	1 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)

Syntax hints:   → wi 4   class class class wbr 5143   ≈ cen 8982   ≼ cdom 8983

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-f1o 6568  df-en 8986  df-dom 8987

This theorem is referenced by:  bren2  9023  domrefg  9027  endomtr  9052  domentr  9053  domunsncan  9112  sbthb  9134  dom0  9142  sdomentr  9151  ensdomtr  9153  domtriord  9163  domunsn  9167  xpen  9180  sdomdomtrfi  9241  domsdomtrfi  9242  sucdom2  9243  php  9247  php3  9249  onomeneq  9265  0sdom1dom  9274  rex2dom  9282  unxpdom2  9290  sucxpdom  9291  f1finf1o  9305  findcard3  9318  fodomfi  9350  wdomen1  9616  wdomen2  9617  fidomtri2  10034  prdom2  10046  acnen  10093  acnen2  10095  alephdom  10121  alephinit  10135  undjudom  10208  pwdjudom  10255  fin1a2lem11  10450  hsmexlem1  10466  gchdomtri  10669  gchdjuidm  10708  gchxpidm  10709  gchpwdom  10710  gchhar  10719  gruina  10858  nnct  14022  odinf  19581  hauspwdom  23509  ufildom1  23934  iscmet3  25327  mbfaddlem  25695  ctbssinf  37407  pibt2  37418  heiborlem3  37820  zct  45066  qct  45373  caratheodory  46543