Theorem elpw2 5341

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

Syntax hints:   ↔ wb 205   ∈ wcel 2099  Vcvv 3469   ⊆ wss 3944  𝒫 cpw 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-in 3951  df-ss 3961  df-pw 4600

This theorem is referenced by:  elpwi2  5342  axpweq  5344  knatar  7359  dffi3  9440  marypha1lem  9442  r1pwss  9793  rankr1bg  9812  pwwf  9816  unwf  9819  rankval2  9827  uniwf  9828  rankpwi  9832  dfac2a  10138  dfac12lem2  10153  axdc4lem  10464  axdclem  10528  incexclem  15800  rpnnen2lem1  16176  rpnnen2lem2  16177  sadfval  16412  smufval  16437  smupf  16438  vdwapf  16926  prdshom  17434  mreacs  17623  acsfn  17624  lubeldm  18330  lubval  18333  glbeldm  18343  glbval  18346  clatlem  18479  clatlubcl2  18481  clatglbcl2  18483  issubmgm  18647  issubm  18740  issubg  19065  cntzval  19256  sylow1lem2  19538  lsmvalx  19578  pj1fval  19633  issubrng  20466  issubrg  20492  islss  20800  lspval  20841  lspcl  20842  islbs  20943  lbsextlem1  21028  lbsextlem3  21030  lbsextlem4  21031  sraval  21042  ocvval  21579  isobs  21634  islinds  21723  aspval  21786  uncmp  23281  cmpfi  23286  cmpfii  23287  2ndc1stc  23329  1stcrest  23331  hausllycmp  23372  lly1stc  23374  1stckgenlem  23431  txlly  23514  txnlly  23515  tx1stc  23528  basqtop  23589  tgqtop  23590  alexsubALTlem3  23927  alexsubALTlem4  23928  alexsubALT  23929  cncfval  24782  cnllycmp  24856  ovolficcss  25372  ovolval  25376  ovolicc2  25425  ismbl  25429  mblsplit  25435  voliunlem3  25455  vitalilem4  25514  vitalilem5  25515  dvfval  25800  dvnfval  25826  cpnfval  25836  plyval  26101  dmarea  26863  wilthlem2  26975  issh  30992  ocval  31064  spanval  31117  hsupval  31118  sshjval  31134  sshjval3  31138  zarcls  33398  zartopn  33399  sigagensiga  33683  dya2iocuni  33826  coinflippv  34026  ballotlemelo  34030  ballotth  34080  erdszelem1  34724  kur14lem9  34747  kur14  34749  cnllysconn  34778  elmpst  35069  mclsrcl  35094  mclsval  35096  icoreresf  36754  cntotbnd  37191  heibor1lem  37204  heibor  37216  isidl  37409  igenval  37456  paddval  39195  pclvalN  39287  polvalN  39302  docavalN  40520  djavalN  40532  dicval  40573  dochval  40748  djhval  40795  lpolconN  40884  elpwbi  41627  elmzpcl  42058  eldiophb  42089  rpnnen3  42365  islssfgi  42408  hbt  42466  elmnc  42472  itgoval  42497  itgocn  42500  rgspnval  42504  elpglem2  48056