Theorem elpw2 5212

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

Syntax hints:   ↔ wb 209   ∈ wcel 2111  Vcvv 3441   ⊆ wss 3881  𝒫 cpw 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  elpwi2  5213  axpweq  5230  knatar  7089  dffi3  8879  marypha1lem  8881  r1pwss  9197  rankr1bg  9216  pwwf  9220  unwf  9223  rankval2  9231  uniwf  9232  rankpwi  9236  dfac2a  9540  dfac12lem2  9555  axdc4lem  9866  axdclem  9930  incexclem  15183  rpnnen2lem1  15559  rpnnen2lem2  15560  sadfval  15791  smufval  15816  smupf  15817  vdwapf  16298  prdshom  16732  mreacs  16921  acsfn  16922  lubeldm  17583  lubval  17586  glbeldm  17596  glbval  17599  clatlem  17713  clatlubcl2  17715  clatglbcl2  17717  issubm  17960  issubg  18271  cntzval  18443  sylow1lem2  18716  lsmvalx  18756  pj1fval  18812  issubrg  19528  islss  19699  lspval  19740  lspcl  19741  islbs  19841  lbsextlem1  19923  lbsextlem3  19925  lbsextlem4  19926  sraval  19941  ocvval  20356  isobs  20409  islinds  20498  aspval  20559  uncmp  22008  cmpfi  22013  cmpfii  22014  2ndc1stc  22056  1stcrest  22058  hausllycmp  22099  lly1stc  22101  1stckgenlem  22158  txlly  22241  txnlly  22242  tx1stc  22255  basqtop  22316  tgqtop  22317  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  cncfval  23493  cnllycmp  23561  ovolficcss  24073  ovolval  24077  ovolicc2  24126  ismbl  24130  mblsplit  24136  voliunlem3  24156  vitalilem4  24215  vitalilem5  24216  dvfval  24500  dvnfval  24525  cpnfval  24535  plyval  24790  dmarea  25543  wilthlem2  25654  issh  28991  ocval  29063  spanval  29116  hsupval  29117  sshjval  29133  sshjval3  29137  zarcls  31227  zartopn  31228  sigagensiga  31510  dya2iocuni  31651  coinflippv  31851  ballotlemelo  31855  ballotth  31905  erdszelem1  32551  kur14lem9  32574  kur14  32576  cnllysconn  32605  elmpst  32896  mclsrcl  32921  mclsval  32923  icoreresf  34769  cntotbnd  35234  heibor1lem  35247  heibor  35259  isidl  35452  igenval  35499  paddval  37094  pclvalN  37186  polvalN  37201  docavalN  38419  djavalN  38431  dicval  38472  dochval  38647  djhval  38694  lpolconN  38783  elpwbi  39410  elmzpcl  39667  eldiophb  39698  rpnnen3  39973  islssfgi  40016  hbt  40074  elmnc  40080  itgoval  40105  itgocn  40108  rgspnval  40112  issubmgm  44409  elpglem2  45241