Theorem elpw2 5346

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

Syntax hints:   ↔ wb 205   ∈ wcel 2104  Vcvv 3472   ⊆ wss 3949  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  elpwi2  5347  axpweq  5349  knatar  7358  dffi3  9430  marypha1lem  9432  r1pwss  9783  rankr1bg  9802  pwwf  9806  unwf  9809  rankval2  9817  uniwf  9818  rankpwi  9822  dfac2a  10128  dfac12lem2  10143  axdc4lem  10454  axdclem  10518  incexclem  15788  rpnnen2lem1  16163  rpnnen2lem2  16164  sadfval  16399  smufval  16424  smupf  16425  vdwapf  16911  prdshom  17419  mreacs  17608  acsfn  17609  lubeldm  18312  lubval  18315  glbeldm  18325  glbval  18328  clatlem  18461  clatlubcl2  18463  clatglbcl2  18465  issubmgm  18629  issubm  18722  issubg  19044  cntzval  19228  sylow1lem2  19510  lsmvalx  19550  pj1fval  19605  issubrng  20437  issubrg  20463  islss  20691  lspval  20732  lspcl  20733  islbs  20833  lbsextlem1  20918  lbsextlem3  20920  lbsextlem4  20921  sraval  20936  ocvval  21441  isobs  21496  islinds  21585  aspval  21648  uncmp  23129  cmpfi  23134  cmpfii  23135  2ndc1stc  23177  1stcrest  23179  hausllycmp  23220  lly1stc  23222  1stckgenlem  23279  txlly  23362  txnlly  23363  tx1stc  23376  basqtop  23437  tgqtop  23438  alexsubALTlem3  23775  alexsubALTlem4  23776  alexsubALT  23777  cncfval  24630  cnllycmp  24704  ovolficcss  25220  ovolval  25224  ovolicc2  25273  ismbl  25277  mblsplit  25283  voliunlem3  25303  vitalilem4  25362  vitalilem5  25363  dvfval  25648  dvnfval  25673  cpnfval  25683  plyval  25941  dmarea  26696  wilthlem2  26807  issh  30726  ocval  30798  spanval  30851  hsupval  30852  sshjval  30868  sshjval3  30872  zarcls  33150  zartopn  33151  sigagensiga  33435  dya2iocuni  33578  coinflippv  33778  ballotlemelo  33782  ballotth  33832  erdszelem1  34478  kur14lem9  34501  kur14  34503  cnllysconn  34532  elmpst  34823  mclsrcl  34848  mclsval  34850  icoreresf  36538  cntotbnd  36969  heibor1lem  36982  heibor  36994  isidl  37187  igenval  37234  paddval  38974  pclvalN  39066  polvalN  39081  docavalN  40299  djavalN  40311  dicval  40352  dochval  40527  djhval  40574  lpolconN  40663  elpwbi  41357  elmzpcl  41768  eldiophb  41799  rpnnen3  42075  islssfgi  42118  hbt  42176  elmnc  42182  itgoval  42207  itgocn  42210  rgspnval  42214  elpglem2  47846