Theorem elpw2 5269

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

Step	Hyp	Ref	Expression
1		elpw2.1	. 2 ⊢ 𝐵 ∈ V
2		elpw2g 5268	. 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 205   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  elpwi2  5270  axpweq  5287  knatar  7228  dffi3  9190  marypha1lem  9192  r1pwss  9542  rankr1bg  9561  pwwf  9565  unwf  9568  rankval2  9576  uniwf  9577  rankpwi  9581  dfac2a  9885  dfac12lem2  9900  axdc4lem  10211  axdclem  10275  incexclem  15548  rpnnen2lem1  15923  rpnnen2lem2  15924  sadfval  16159  smufval  16184  smupf  16185  vdwapf  16673  prdshom  17178  mreacs  17367  acsfn  17368  lubeldm  18071  lubval  18074  glbeldm  18084  glbval  18087  clatlem  18220  clatlubcl2  18222  clatglbcl2  18224  issubm  18442  issubg  18755  cntzval  18927  sylow1lem2  19204  lsmvalx  19244  pj1fval  19300  issubrg  20024  islss  20196  lspval  20237  lspcl  20238  islbs  20338  lbsextlem1  20420  lbsextlem3  20422  lbsextlem4  20423  sraval  20438  ocvval  20872  isobs  20927  islinds  21016  aspval  21077  uncmp  22554  cmpfi  22559  cmpfii  22560  2ndc1stc  22602  1stcrest  22604  hausllycmp  22645  lly1stc  22647  1stckgenlem  22704  txlly  22787  txnlly  22788  tx1stc  22801  basqtop  22862  tgqtop  22863  alexsubALTlem3  23200  alexsubALTlem4  23201  alexsubALT  23202  cncfval  24051  cnllycmp  24119  ovolficcss  24633  ovolval  24637  ovolicc2  24686  ismbl  24690  mblsplit  24696  voliunlem3  24716  vitalilem4  24775  vitalilem5  24776  dvfval  25061  dvnfval  25086  cpnfval  25096  plyval  25354  dmarea  26107  wilthlem2  26218  issh  29570  ocval  29642  spanval  29695  hsupval  29696  sshjval  29712  sshjval3  29716  zarcls  31824  zartopn  31825  sigagensiga  32109  dya2iocuni  32250  coinflippv  32450  ballotlemelo  32454  ballotth  32504  erdszelem1  33153  kur14lem9  33176  kur14  33178  cnllysconn  33207  elmpst  33498  mclsrcl  33523  mclsval  33525  icoreresf  35523  cntotbnd  35954  heibor1lem  35967  heibor  35979  isidl  36172  igenval  36219  paddval  37812  pclvalN  37904  polvalN  37919  docavalN  39137  djavalN  39149  dicval  39190  dochval  39365  djhval  39412  lpolconN  39501  elpwbi  40205  elmzpcl  40548  eldiophb  40579  rpnnen3  40854  islssfgi  40897  hbt  40955  elmnc  40961  itgoval  40986  itgocn  40989  rgspnval  40993  issubmgm  45343  elpglem2  46417