Theorem elpw2 5295

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 5294	. 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-pw 4558

This theorem is used by:  elpwi2  5296  axpweq  5311  knatar  7367  dffi3  9423  marypha1lem  9425  r1pwss  9791  rankr1bg  9811  pwwf  9815  unwf  9818  rankval2  9827  uniwf  9828  rankpwi  9832  rankval2b  9835  dfac2a  10208  dfac12lem2  10223  axdc4lem  10533  axdclem  10597  incexclem  16005  rpnnen2lem1  16382  rpnnen2lem2  16383  sadfval  16622  smufval  16647  smupf  16648  vdwapf  17150  prdshom  17638  mreacs  17832  acsfn  17833  lubeldm  18525  lubval  18528  glbeldm  18538  glbval  18541  clatlem  18676  clatlubcl2  18678  clatglbcl2  18680  issubmgm  18891  issubm  18998  issubg  19336  cntzval  19535  sylow1lem2  19813  lsmvalx  19853  pj1fval  19908  issubrng  20799  issubrg  20823  rgspnval  20864  islss  21209  lspval  21250  lspcl  21251  islbs  21351  lbsextlem1  21436  lbsextlem3  21438  lbsextlem4  21439  sraval  21450  ocvval  21973  isobs  22026  islinds  22115  aspval  22180  uncmp  23721  cmpfi  23726  cmpfii  23727  2ndc1stc  23769  1stcrest  23771  hausllycmp  23813  lly1stc  23815  1stckgenlem  23872  txlly  23955  txnlly  23956  tx1stc  23969  basqtop  24030  tgqtop  24031  alexsubALTlem3  24368  alexsubALTlem4  24369  alexsubALT  24370  cncfval  25209  cnllycmp  25277  ovolficcss  25790  ovolval  25794  ovolicc2  25843  ismbl  25847  mblsplit  25853  voliunlem3  25873  vitalilem4  25932  vitalilem5  25933  dvfval  26217  dvnfval  26242  cpnfval  26252  plyval  26511  dmarea  27285  wilthlem2  27396  issh  31810  ocval  31882  spanval  31935  hsupval  31936  sshjval  31952  sshjval3  31956  zarcls  34548  zartopn  34549  sigagensiga  34816  dya2iocuni  34957  coinflippv  35158  ballotlemelo  35162  ballotth  35212  r1ssel  35774  erdszelem1  35998  kur14lem9  36021  kur14  36023  cnllysconn  36052  elmpst  36343  mclsrcl  36368  mclsval  36370  ttcwf  37354  icoreresf  38318  cntotbnd  38773  heibor1lem  38786  heibor  38798  isidl  38991  igenval  39038  paddval  40898  pclvalN  40990  polvalN  41005  docavalN  42223  djavalN  42235  dicval  42276  dochval  42451  djhval  42498  lpolconN  42587  elpwbi  43327  elmzpcl  43780  eldiophb  43811  rpnnen3  44082  islssfgi  44117  hbt  44175  elmnc  44181  itgoval  44206  itgocn  44209  elpglem2  50848