Theorem elpw2 5304

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

Syntax hints:   ↔ wb 209   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3904  𝒫 cpw 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-in 3911  df-ss 3921  df-pw 4563

This theorem is referenced by:  elpwi2  5305  axpweq  5321  knatar  7355  dffi3  9390  marypha1lem  9392  r1pwss  9755  rankr1bg  9774  pwwf  9778  unwf  9781  rankval2  9789  uniwf  9790  rankpwi  9794  dfac2a  10112  dfac12lem2  10127  axdc4lem  10438  axdclem  10502  incexclem  15889  rpnnen2lem1  16269  rpnnen2lem2  16270  sadfval  16509  smufval  16534  smupf  16535  vdwapf  17031  prdshom  17519  mreacs  17713  acsfn  17714  lubeldm  18406  lubval  18409  glbeldm  18419  glbval  18422  clatlem  18557  clatlubcl2  18559  clatglbcl2  18561  issubmgm  18759  issubm  18860  issubg  19191  cntzval  19390  sylow1lem2  19668  lsmvalx  19708  pj1fval  19763  issubrng  20631  issubrg  20655  rgspnval  20696  islss  21034  lspval  21075  lspcl  21076  islbs  21176  lbsextlem1  21261  lbsextlem3  21263  lbsextlem4  21264  sraval  21275  ocvval  21796  isobs  21849  islinds  21938  aspval  22001  uncmp  23539  cmpfi  23544  cmpfii  23545  2ndc1stc  23587  1stcrest  23589  hausllycmp  23630  lly1stc  23632  1stckgenlem  23689  txlly  23772  txnlly  23773  tx1stc  23786  basqtop  23847  tgqtop  23848  alexsubALTlem3  24185  alexsubALTlem4  24186  alexsubALT  24187  cncfval  25026  cnllycmp  25094  ovolficcss  25607  ovolval  25611  ovolicc2  25660  ismbl  25664  mblsplit  25670  voliunlem3  25690  vitalilem4  25749  vitalilem5  25750  dvfval  26035  dvnfval  26060  cpnfval  26070  plyval  26329  dmarea  27098  wilthlem2  27209  issh  31526  ocval  31598  spanval  31651  hsupval  31652  sshjval  31668  sshjval3  31672  zarcls  34230  zartopn  34231  sigagensiga  34497  dya2iocuni  34639  coinflippv  34840  ballotlemelo  34844  ballotth  34894  rankval2b  35456  r1ssel  35465  erdszelem1  35637  kur14lem9  35660  kur14  35662  cnllysconn  35691  elmpst  35982  mclsrcl  36007  mclsval  36009  ttcwf  36979  icoreresf  37942  cntotbnd  38391  heibor1lem  38404  heibor  38416  isidl  38609  igenval  38656  paddval  40518  pclvalN  40610  polvalN  40625  docavalN  41843  djavalN  41855  dicval  41896  dochval  42071  djhval  42118  lpolconN  42207  elpwbi  42947  elmzpcl  43405  eldiophb  43436  rpnnen3  43707  islssfgi  43747  hbt  43805  elmnc  43811  itgoval  43836  itgocn  43839  elpglem2  50435