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

Theorem endom 9006
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 9004 . 2 ≈ ⊆ ≼
21ssbri 5197 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   class class class wbr 5152  cen 8967  cdom 8968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5688  df-rel 5689  df-f1o 6560  df-en 8971  df-dom 8972
This theorem is referenced by:  bren2  9010  domrefg  9014  endomtr  9039  domentr  9040  domunsncan  9103  sbthb  9125  dom0  9133  sdomentr  9142  ensdomtr  9144  domtriord  9154  domunsn  9158  xpen  9171  sdomdomtrfi  9235  domsdomtrfi  9236  sucdom2  9237  php  9241  php3  9243  onomeneq  9259  0sdom1dom  9269  rex2dom  9277  unxpdom2  9285  sucxpdom  9286  f1finf1o  9302  findcard3  9316  wdomen1  9607  wdomen2  9608  fidomtri2  10025  prdom2  10037  acnen  10084  acnen2  10086  alephdom  10112  alephinit  10126  undjudom  10198  pwdjudom  10247  fin1a2lem11  10441  hsmexlem1  10457  gchdomtri  10660  gchdjuidm  10699  gchxpidm  10700  gchpwdom  10701  gchhar  10710  gruina  10849  nnct  13986  odinf  19525  hauspwdom  23425  ufildom1  23850  iscmet3  25241  mbfaddlem  25609  ctbssinf  36918  pibt2  36929  heiborlem3  37319  zct  44456  qct  44773  caratheodory  45945
  Copyright terms: Public domain W3C validator