Theorem elpw2 5269

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  𝒫 cpw 4542

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 5231

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 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  elpwi2  5270  axpweq  5286  knatar  7303  dffi3  9335  marypha1lem  9337  r1pwss  9697  rankr1bg  9716  pwwf  9720  unwf  9723  rankval2  9731  uniwf  9732  rankpwi  9736  dfac2a  10041  dfac12lem2  10056  axdc4lem  10366  axdclem  10430  incexclem  15760  rpnnen2lem1  16140  rpnnen2lem2  16141  sadfval  16380  smufval  16405  smupf  16406  vdwapf  16901  prdshom  17388  mreacs  17582  acsfn  17583  lubeldm  18275  lubval  18278  glbeldm  18288  glbval  18291  clatlem  18426  clatlubcl2  18428  clatglbcl2  18430  issubmgm  18628  issubm  18729  issubg  19060  cntzval  19254  sylow1lem2  19532  lsmvalx  19572  pj1fval  19627  issubrng  20482  issubrg  20506  rgspnval  20547  islss  20887  lspval  20928  lspcl  20929  islbs  21030  lbsextlem1  21115  lbsextlem3  21117  lbsextlem4  21118  sraval  21129  ocvval  21624  isobs  21677  islinds  21766  aspval  21829  uncmp  23346  cmpfi  23351  cmpfii  23352  2ndc1stc  23394  1stcrest  23396  hausllycmp  23437  lly1stc  23439  1stckgenlem  23496  txlly  23579  txnlly  23580  tx1stc  23593  basqtop  23654  tgqtop  23655  alexsubALTlem3  23992  alexsubALTlem4  23993  alexsubALT  23994  cncfval  24833  cnllycmp  24901  ovolficcss  25414  ovolval  25418  ovolicc2  25467  ismbl  25471  mblsplit  25477  voliunlem3  25497  vitalilem4  25556  vitalilem5  25557  dvfval  25842  dvnfval  25867  cpnfval  25877  plyval  26139  dmarea  26907  wilthlem2  27019  issh  31268  ocval  31340  spanval  31393  hsupval  31394  sshjval  31410  sshjval3  31414  zarcls  34024  zartopn  34025  sigagensiga  34291  dya2iocuni  34433  coinflippv  34634  ballotlemelo  34638  ballotth  34688  rankval2b  35248  r1ssel  35256  erdszelem1  35379  kur14lem9  35402  kur14  35404  cnllysconn  35433  elmpst  35724  mclsrcl  35749  mclsval  35751  ttcwf  36712  icoreresf  37664  cntotbnd  38108  heibor1lem  38121  heibor  38133  isidl  38326  igenval  38373  paddval  40235  pclvalN  40327  polvalN  40342  docavalN  41560  djavalN  41572  dicval  41613  dochval  41788  djhval  41835  lpolconN  41924  elpwbi  42663  elmzpcl  43157  eldiophb  43188  rpnnen3  43463  islssfgi  43503  hbt  43561  elmnc  43567  itgoval  43592  itgocn  43595  elpglem2  50145