MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpw2 Unicode version

Theorem elpw2 4191
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
Hypothesis
Ref Expression
elpw2.1  |-  B  e. 
_V
Assertion
Ref Expression
elpw2  |-  ( A  e.  ~P B  <->  A  C_  B
)

Proof of Theorem elpw2
StepHypRef Expression
1 elpw2.1 . 2  |-  B  e. 
_V
2 elpw2g 4190 . 2  |-  ( B  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
31, 2ax-mp 8 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1696   _Vcvv 2801    C_ wss 3165   ~Pcpw 3638
This theorem is referenced by:  axpweq  4203  abexssex  5797  knatar  5873  canth  6310  dffi3  7200  marypha1lem  7202  r1pwss  7472  rankr1bg  7491  pwwf  7495  unwf  7498  rankval2  7506  uniwf  7507  rankpwi  7511  aceq3lem  7763  dfac2a  7772  dfac12lem2  7786  cflim3  7904  cflim2  7905  cfslb  7908  axdc3lem4  8095  axdc4lem  8097  axdclem  8162  grothpw  8464  uzf  10249  ixxf  10682  fzf  10802  incexclem  12311  rpnnen2lem1  12509  rpnnen2lem2  12510  bitsf  12634  sadfval  12659  smufval  12684  smupf  12685  vdwapf  13035  prdsval  13371  prdsds  13379  prdshom  13382  mreacs  13576  acsfn  13577  wunnat  13846  lubval  14129  glbval  14134  clatlem  14232  issubm  14441  issubg  14637  cntzval  14813  sylow1lem2  14926  lsmvalx  14966  pj1fval  15019  issubrg  15561  islss  15708  lspval  15748  lspcl  15749  islbs  15845  lbsextlem1  15927  lbsextlem3  15929  lbsextlem4  15930  sraval  15945  aspval  16084  ocvfval  16582  ocvval  16583  isobs  16636  leordtval2  16958  cnpfval  16980  iscnp2  16985  uncmp  17146  cmpfi  17151  cmpfii  17152  2ndc1stc  17193  1stcrest  17195  islly2  17226  hausllycmp  17236  lly1stc  17238  1stckgenlem  17264  xkotf  17296  txlly  17346  txnlly  17347  tx1stc  17360  basqtop  17418  tgqtop  17419  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  cncfval  18408  cnllycmp  18470  bndth  18472  ishtpy  18486  ovolficcss  18845  ovolval  18849  ovolicc2  18897  ismbl  18901  mblsplit  18907  voliunlem2  18924  voliunlem3  18925  vitalilem4  18982  vitalilem5  18983  dvfval  19263  dvnfval  19287  cpnfval  19297  plyval  19591  dmarea  20268  wilthlem2  20323  issh  21803  ocval  21875  spanval  21928  hsupval  21929  sshjval  21945  sshjval3  21949  erdszelem1  23737  kur14lem9  23760  kur14  23762  cnllyscon  23791  umgrabi  23922  isidlNEW  25549  vtarsuelt  25998  cover2  26461  cntotbnd  26623  heibor1lem  26636  heibor  26648  isidl  26742  igenval  26789  elmzpcl  26907  eldiophb  26939  rpnnen3  27228  islssfgi  27273  islinds  27382  hbt  27437  elmnc  27444  itgoval  27469  itgocn  27472  rgspnval  27476  paddval  30609  pclvalN  30701  polvalN  30716  docavalN  31935  djavalN  31947  dicval  31988  dochval  32163  djhval  32210  lpolconN  32299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640
  Copyright terms: Public domain W3C validator