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

Theorem elpw2 5240
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 5239 . 2 (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2105  Vcvv 3495  wss 3935  𝒫 cpw 4537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-in 3942  df-ss 3951  df-pw 4539
This theorem is referenced by:  axpweq  5257  knatar  7099  dffi3  8884  marypha1lem  8886  r1pwss  9202  rankr1bg  9221  pwwf  9225  unwf  9228  rankval2  9236  uniwf  9237  rankpwi  9241  dfac2a  9544  dfac12lem2  9559  axdc4lem  9866  axdclem  9930  incexclem  15181  rpnnen2lem1  15557  rpnnen2lem2  15558  sadfval  15791  smufval  15816  smupf  15817  vdwapf  16298  prdshom  16730  mreacs  16919  acsfn  16920  lubeldm  17581  lubval  17584  glbeldm  17594  glbval  17597  clatlem  17711  clatlubcl2  17713  clatglbcl2  17715  issubm  17958  issubg  18219  cntzval  18391  sylow1lem2  18655  lsmvalx  18695  pj1fval  18751  issubrg  19466  islss  19637  lspval  19678  lspcl  19679  islbs  19779  lbsextlem1  19861  lbsextlem3  19863  lbsextlem4  19864  sraval  19879  aspval  20032  ocvval  20741  isobs  20794  islinds  20883  uncmp  21941  cmpfi  21946  cmpfii  21947  2ndc1stc  21989  1stcrest  21991  hausllycmp  22032  lly1stc  22034  1stckgenlem  22091  txlly  22174  txnlly  22175  tx1stc  22188  basqtop  22249  tgqtop  22250  alexsubALTlem3  22587  alexsubALTlem4  22588  alexsubALT  22589  cncfval  23425  cnllycmp  23489  ovolficcss  23999  ovolval  24003  ovolicc2  24052  ismbl  24056  mblsplit  24062  voliunlem3  24082  vitalilem4  24141  vitalilem5  24142  dvfval  24424  dvnfval  24448  cpnfval  24458  plyval  24712  dmarea  25463  wilthlem2  25574  issh  28913  ocval  28985  spanval  29038  hsupval  29039  sshjval  29055  sshjval3  29059  sigagensiga  31300  dya2iocuni  31441  coinflippv  31641  ballotlemelo  31645  ballotth  31695  erdszelem1  32336  kur14lem9  32359  kur14  32361  cnllysconn  32390  elmpst  32681  mclsrcl  32706  mclsval  32708  icoreresf  34516  cntotbnd  34957  heibor1lem  34970  heibor  34982  isidl  35175  igenval  35222  paddval  36816  pclvalN  36908  polvalN  36923  docavalN  38141  djavalN  38153  dicval  38194  dochval  38369  djhval  38416  lpolconN  38505  elpwbi  38996  elmzpcl  39203  eldiophb  39234  rpnnen3  39509  islssfgi  39552  hbt  39610  elmnc  39616  itgoval  39641  itgocn  39644  rgspnval  39648  issubmgm  43903  elpglem2  44712
  Copyright terms: Public domain W3C validator