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 208   ∈ wcel 2132  Vcvv 3444   ⊆ wss 3895  𝒫 cpw 4545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1097  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-in 3902  df-ss 3912  df-pw 4547

This theorem is referenced by:  elpwi2  5281  axpweq  5297  knatar  7326  dffi3  9363  marypha1lem  9365  r1pwss  9728  rankr1bg  9747  pwwf  9751  unwf  9754  rankval2  9762  uniwf  9763  rankpwi  9767  dfac2a  10072  dfac12lem2  10087  axdc4lem  10398  axdclem  10462  incexclem  15838  rpnnen2lem1  16218  rpnnen2lem2  16219  sadfval  16458  smufval  16483  smupf  16484  vdwapf  16980  prdshom  17468  mreacs  17662  acsfn  17663  lubeldm  18355  lubval  18358  glbeldm  18368  glbval  18371  clatlem  18506  clatlubcl2  18508  clatglbcl2  18510  issubmgm  18708  issubm  18809  issubg  19140  cntzval  19333  sylow1lem2  19611  lsmvalx  19651  pj1fval  19706  issubrng  20565  issubrg  20589  rgspnval  20630  islss  20970  lspval  21011  lspcl  21012  islbs  21112  lbsextlem1  21197  lbsextlem3  21199  lbsextlem4  21200  sraval  21211  ocvval  21688  isobs  21741  islinds  21830  aspval  21893  uncmp  23432  cmpfi  23437  cmpfii  23438  2ndc1stc  23480  1stcrest  23482  hausllycmp  23523  lly1stc  23525  1stckgenlem  23582  txlly  23665  txnlly  23666  tx1stc  23679  basqtop  23740  tgqtop  23741  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  cncfval  24919  cnllycmp  24987  ovolficcss  25500  ovolval  25504  ovolicc2  25553  ismbl  25557  mblsplit  25563  voliunlem3  25583  vitalilem4  25642  vitalilem5  25643  dvfval  25928  dvnfval  25953  cpnfval  25963  plyval  26222  dmarea  26988  wilthlem2  27099  issh  31346  ocval  31418  spanval  31471  hsupval  31472  sshjval  31488  sshjval3  31492  zarcls  34115  zartopn  34116  sigagensiga  34382  dya2iocuni  34524  coinflippv  34725  ballotlemelo  34729  ballotth  34779  rankval2b  35340  r1ssel  35348  erdszelem1  35479  kur14lem9  35502  kur14  35504  cnllysconn  35533  elmpst  35824  mclsrcl  35849  mclsval  35851  ttcwf  36822  icoreresf  37784  cntotbnd  38233  heibor1lem  38246  heibor  38258  isidl  38451  igenval  38498  paddval  40360  pclvalN  40452  polvalN  40467  docavalN  41685  djavalN  41697  dicval  41738  dochval  41913  djhval  41960  lpolconN  42049  elpwbi  42787  elmzpcl  43245  eldiophb  43276  rpnnen3  43547  islssfgi  43587  hbt  43645  elmnc  43651  itgoval  43676  itgocn  43679  elpglem2  50271