Theorem elpw2 5276

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3438   ⊆ wss 3905  𝒫 cpw 4553

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-in 3912  df-ss 3922  df-pw 4555

This theorem is referenced by:  elpwi2  5277  axpweq  5293  knatar  7298  dffi3  9340  marypha1lem  9342  r1pwss  9699  rankr1bg  9718  pwwf  9722  unwf  9725  rankval2  9733  uniwf  9734  rankpwi  9738  dfac2a  10043  dfac12lem2  10058  axdc4lem  10368  axdclem  10432  incexclem  15761  rpnnen2lem1  16141  rpnnen2lem2  16142  sadfval  16381  smufval  16406  smupf  16407  vdwapf  16902  prdshom  17389  mreacs  17582  acsfn  17583  lubeldm  18275  lubval  18278  glbeldm  18288  glbval  18291  clatlem  18426  clatlubcl2  18428  clatglbcl2  18430  issubmgm  18594  issubm  18695  issubg  19023  cntzval  19218  sylow1lem2  19496  lsmvalx  19536  pj1fval  19591  issubrng  20450  issubrg  20474  rgspnval  20515  islss  20855  lspval  20896  lspcl  20897  islbs  20998  lbsextlem1  21083  lbsextlem3  21085  lbsextlem4  21086  sraval  21097  ocvval  21592  isobs  21645  islinds  21734  aspval  21798  uncmp  23306  cmpfi  23311  cmpfii  23312  2ndc1stc  23354  1stcrest  23356  hausllycmp  23397  lly1stc  23399  1stckgenlem  23456  txlly  23539  txnlly  23540  tx1stc  23553  basqtop  23614  tgqtop  23615  alexsubALTlem3  23952  alexsubALTlem4  23953  alexsubALT  23954  cncfval  24797  cnllycmp  24871  ovolficcss  25386  ovolval  25390  ovolicc2  25439  ismbl  25443  mblsplit  25449  voliunlem3  25469  vitalilem4  25528  vitalilem5  25529  dvfval  25814  dvnfval  25840  cpnfval  25850  plyval  26114  dmarea  26883  wilthlem2  26995  issh  31170  ocval  31242  spanval  31295  hsupval  31296  sshjval  31312  sshjval3  31316  zarcls  33840  zartopn  33841  sigagensiga  34107  dya2iocuni  34250  coinflippv  34451  ballotlemelo  34455  ballotth  34505  erdszelem1  35163  kur14lem9  35186  kur14  35188  cnllysconn  35217  elmpst  35508  mclsrcl  35533  mclsval  35535  icoreresf  37325  cntotbnd  37775  heibor1lem  37788  heibor  37800  isidl  37993  igenval  38040  paddval  39777  pclvalN  39869  polvalN  39884  docavalN  41102  djavalN  41114  dicval  41155  dochval  41330  djhval  41377  lpolconN  41466  elpwbi  42203  elmzpcl  42699  eldiophb  42730  rpnnen3  43005  islssfgi  43045  hbt  43103  elmnc  43109  itgoval  43134  itgocn  43137  elpglem2  49685