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

Theorem elpw2 5234
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
Hypothesis
Ref Expression
elpw2.1 𝐵 ∈ V
Assertion
Ref Expression
elpw2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)

Proof of Theorem elpw2
StepHypRef Expression
1 elpw2.1 . 2 𝐵 ∈ V
2 elpw2g 5233 . 2 (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wcel 2115  Vcvv 3480  wss 3919  𝒫 cpw 4522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-sep 5189
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-v 3482  df-in 3926  df-ss 3936  df-pw 4524
This theorem is referenced by:  elpwi2  5235  axpweq  5252  knatar  7103  dffi3  8892  marypha1lem  8894  r1pwss  9210  rankr1bg  9229  pwwf  9233  unwf  9236  rankval2  9244  uniwf  9245  rankpwi  9249  dfac2a  9553  dfac12lem2  9568  axdc4lem  9875  axdclem  9939  incexclem  15191  rpnnen2lem1  15567  rpnnen2lem2  15568  sadfval  15799  smufval  15824  smupf  15825  vdwapf  16306  prdshom  16740  mreacs  16929  acsfn  16930  lubeldm  17591  lubval  17594  glbeldm  17604  glbval  17607  clatlem  17721  clatlubcl2  17723  clatglbcl2  17725  issubm  17968  issubg  18279  cntzval  18451  sylow1lem2  18724  lsmvalx  18764  pj1fval  18820  issubrg  19535  islss  19706  lspval  19747  lspcl  19748  islbs  19848  lbsextlem1  19930  lbsextlem3  19932  lbsextlem4  19933  sraval  19948  ocvval  20363  isobs  20416  islinds  20505  aspval  20566  uncmp  22014  cmpfi  22019  cmpfii  22020  2ndc1stc  22062  1stcrest  22064  hausllycmp  22105  lly1stc  22107  1stckgenlem  22164  txlly  22247  txnlly  22248  tx1stc  22261  basqtop  22322  tgqtop  22323  alexsubALTlem3  22660  alexsubALTlem4  22661  alexsubALT  22662  cncfval  23499  cnllycmp  23567  ovolficcss  24079  ovolval  24083  ovolicc2  24132  ismbl  24136  mblsplit  24142  voliunlem3  24162  vitalilem4  24221  vitalilem5  24222  dvfval  24506  dvnfval  24531  cpnfval  24541  plyval  24796  dmarea  25549  wilthlem2  25660  issh  28997  ocval  29069  spanval  29122  hsupval  29123  sshjval  29139  sshjval3  29143  sigagensiga  31460  dya2iocuni  31601  coinflippv  31801  ballotlemelo  31805  ballotth  31855  erdszelem1  32498  kur14lem9  32521  kur14  32523  cnllysconn  32552  elmpst  32843  mclsrcl  32868  mclsval  32870  icoreresf  34717  cntotbnd  35182  heibor1lem  35195  heibor  35207  isidl  35400  igenval  35447  paddval  37042  pclvalN  37134  polvalN  37149  docavalN  38367  djavalN  38379  dicval  38420  dochval  38595  djhval  38642  lpolconN  38731  elpwbi  39347  elmzpcl  39587  eldiophb  39618  rpnnen3  39893  islssfgi  39936  hbt  39994  elmnc  40000  itgoval  40025  itgocn  40028  rgspnval  40032  issubmgm  44339  elpglem2  45171
  Copyright terms: Public domain W3C validator