Theorem elpw2 5280

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902  𝒫 cpw 4555

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-in 3909  df-ss 3919  df-pw 4557

This theorem is referenced by:  elpwi2  5281  axpweq  5297  knatar  7305  dffi3  9338  marypha1lem  9340  r1pwss  9700  rankr1bg  9719  pwwf  9723  unwf  9726  rankval2  9734  uniwf  9735  rankpwi  9739  dfac2a  10044  dfac12lem2  10059  axdc4lem  10369  axdclem  10433  incexclem  15763  rpnnen2lem1  16143  rpnnen2lem2  16144  sadfval  16383  smufval  16408  smupf  16409  vdwapf  16904  prdshom  17391  mreacs  17585  acsfn  17586  lubeldm  18278  lubval  18281  glbeldm  18291  glbval  18294  clatlem  18429  clatlubcl2  18431  clatglbcl2  18433  issubmgm  18631  issubm  18732  issubg  19060  cntzval  19254  sylow1lem2  19532  lsmvalx  19572  pj1fval  19627  issubrng  20484  issubrg  20508  rgspnval  20549  islss  20889  lspval  20930  lspcl  20931  islbs  21032  lbsextlem1  21117  lbsextlem3  21119  lbsextlem4  21120  sraval  21131  ocvval  21626  isobs  21679  islinds  21768  aspval  21832  uncmp  23351  cmpfi  23356  cmpfii  23357  2ndc1stc  23399  1stcrest  23401  hausllycmp  23442  lly1stc  23444  1stckgenlem  23501  txlly  23584  txnlly  23585  tx1stc  23598  basqtop  23659  tgqtop  23660  alexsubALTlem3  23997  alexsubALTlem4  23998  alexsubALT  23999  cncfval  24841  cnllycmp  24915  ovolficcss  25430  ovolval  25434  ovolicc2  25483  ismbl  25487  mblsplit  25493  voliunlem3  25513  vitalilem4  25572  vitalilem5  25573  dvfval  25858  dvnfval  25884  cpnfval  25894  plyval  26158  dmarea  26927  wilthlem2  27039  issh  31266  ocval  31338  spanval  31391  hsupval  31392  sshjval  31408  sshjval3  31412  zarcls  34012  zartopn  34013  sigagensiga  34279  dya2iocuni  34421  coinflippv  34622  ballotlemelo  34626  ballotth  34676  rankval2b  35236  r1ssel  35244  erdszelem1  35366  kur14lem9  35389  kur14  35391  cnllysconn  35420  elmpst  35711  mclsrcl  35736  mclsval  35738  icoreresf  37528  cntotbnd  37968  heibor1lem  37981  heibor  37993  isidl  38186  igenval  38233  paddval  40095  pclvalN  40187  polvalN  40202  docavalN  41420  djavalN  41432  dicval  41473  dochval  41648  djhval  41695  lpolconN  41784  elpwbi  42523  elmzpcl  43004  eldiophb  43035  rpnnen3  43310  islssfgi  43350  hbt  43408  elmnc  43414  itgoval  43439  itgocn  43442  elpglem2  49993