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

Theorem elpw2 5341
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 5340 . 2 (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2099  Vcvv 3469  wss 3944  𝒫 cpw 4598
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-in 3951  df-ss 3961  df-pw 4600
This theorem is referenced by:  elpwi2  5342  axpweq  5344  knatar  7359  dffi3  9446  marypha1lem  9448  r1pwss  9799  rankr1bg  9818  pwwf  9822  unwf  9825  rankval2  9833  uniwf  9834  rankpwi  9838  dfac2a  10144  dfac12lem2  10159  axdc4lem  10470  axdclem  10534  incexclem  15806  rpnnen2lem1  16182  rpnnen2lem2  16183  sadfval  16418  smufval  16443  smupf  16444  vdwapf  16932  prdshom  17440  mreacs  17629  acsfn  17630  lubeldm  18336  lubval  18339  glbeldm  18349  glbval  18352  clatlem  18485  clatlubcl2  18487  clatglbcl2  18489  issubmgm  18653  issubm  18746  issubg  19072  cntzval  19263  sylow1lem2  19545  lsmvalx  19585  pj1fval  19640  issubrng  20473  issubrg  20499  islss  20807  lspval  20848  lspcl  20849  islbs  20950  lbsextlem1  21035  lbsextlem3  21037  lbsextlem4  21038  sraval  21049  ocvval  21586  isobs  21641  islinds  21730  aspval  21793  uncmp  23294  cmpfi  23299  cmpfii  23300  2ndc1stc  23342  1stcrest  23344  hausllycmp  23385  lly1stc  23387  1stckgenlem  23444  txlly  23527  txnlly  23528  tx1stc  23541  basqtop  23602  tgqtop  23603  alexsubALTlem3  23940  alexsubALTlem4  23941  alexsubALT  23942  cncfval  24795  cnllycmp  24869  ovolficcss  25385  ovolval  25389  ovolicc2  25438  ismbl  25442  mblsplit  25448  voliunlem3  25468  vitalilem4  25527  vitalilem5  25528  dvfval  25813  dvnfval  25839  cpnfval  25849  plyval  26114  dmarea  26876  wilthlem2  26988  issh  31005  ocval  31077  spanval  31130  hsupval  31131  sshjval  31147  sshjval3  31151  zarcls  33411  zartopn  33412  sigagensiga  33696  dya2iocuni  33839  coinflippv  34039  ballotlemelo  34043  ballotth  34093  erdszelem1  34737  kur14lem9  34760  kur14  34762  cnllysconn  34791  elmpst  35082  mclsrcl  35107  mclsval  35109  icoreresf  36767  cntotbnd  37204  heibor1lem  37217  heibor  37229  isidl  37422  igenval  37469  paddval  39208  pclvalN  39300  polvalN  39315  docavalN  40533  djavalN  40545  dicval  40586  dochval  40761  djhval  40808  lpolconN  40897  elpwbi  41639  elmzpcl  42068  eldiophb  42099  rpnnen3  42375  islssfgi  42418  hbt  42476  elmnc  42482  itgoval  42507  itgocn  42510  rgspnval  42514  elpglem2  48066
  Copyright terms: Public domain W3C validator