Theorem endom 8517

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

Syntax hints:   → wi 4   class class class wbr 5047   ≈ cen 8487   ≼ cdom 8488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5184  ax-nul 5191  ax-pr 5311

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3142  df-v 3483  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-br 5048  df-opab 5110  df-xp 5542  df-rel 5543  df-f1o 6343  df-en 8491  df-dom 8492

This theorem is referenced by:  bren2  8521  domrefg  8525  endomtr  8548  domentr  8549  domunsncan  8598  sbthb  8619  sdomentr  8632  ensdomtr  8634  domtriord  8644  domunsn  8648  xpen  8661  unxpdom2  8707  sucxpdom  8708  wdomen1  9021  wdomen2  9022  fidomtri2  9404  prdom2  9413  acnen  9460  acnen2  9462  alephdom  9488  alephinit  9502  undjudom  9574  pwdjudom  9619  fin1a2lem11  9813  hsmexlem1  9829  gchdomtri  10032  gchdjuidm  10071  gchxpidm  10072  gchpwdom  10073  gchhar  10082  gruina  10221  nnct  13334  odinf  18668  hauspwdom  22087  ufildom1  22512  iscmet3  23874  mbfaddlem  24239  ctbssinf  34698  pibt2  34709  heiborlem3  35118  zct  41408  qct  41715  caratheodory  42895