MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  endom Structured version   Visualization version   GIF version

Theorem endom 8530
Description: Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
Assertion
Ref Expression
endom (𝐴𝐵𝐴𝐵)

Proof of Theorem endom
StepHypRef Expression
1 enssdom 8528 . 2 ≈ ⊆ ≼
21ssbri 5103 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   class class class wbr 5058  cen 8500  cdom 8501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-opab 5121  df-xp 5555  df-rel 5556  df-f1o 6356  df-en 8504  df-dom 8505
This theorem is referenced by:  bren2  8534  domrefg  8538  endomtr  8561  domentr  8562  domunsncan  8611  sbthb  8632  sdomentr  8645  ensdomtr  8647  domtriord  8657  domunsn  8661  xpen  8674  unxpdom2  8720  sucxpdom  8721  wdomen1  9034  wdomen2  9035  fidomtri2  9417  prdom2  9426  acnen  9473  acnen2  9475  alephdom  9501  alephinit  9515  undjudom  9587  pwdjudom  9632  fin1a2lem11  9826  hsmexlem1  9842  gchdomtri  10045  gchdjuidm  10084  gchxpidm  10085  gchpwdom  10086  gchhar  10095  gruina  10234  nnct  13343  odinf  18684  hauspwdom  22103  ufildom1  22528  iscmet3  23890  mbfaddlem  24255  ctbssinf  34681  pibt2  34692  heiborlem3  35085  zct  41316  qct  41623  caratheodory  42804
  Copyright terms: Public domain W3C validator