Theorem elpw2 5270

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

Syntax hints:   ↔ wb 206   ∈ wcel 2110  Vcvv 3434   ⊆ wss 3900  𝒫 cpw 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-in 3907  df-ss 3917  df-pw 4550

This theorem is referenced by:  elpwi2  5271  axpweq  5287  knatar  7286  dffi3  9310  marypha1lem  9312  r1pwss  9669  rankr1bg  9688  pwwf  9692  unwf  9695  rankval2  9703  uniwf  9704  rankpwi  9708  dfac2a  10013  dfac12lem2  10028  axdc4lem  10338  axdclem  10402  incexclem  15735  rpnnen2lem1  16115  rpnnen2lem2  16116  sadfval  16355  smufval  16380  smupf  16381  vdwapf  16876  prdshom  17363  mreacs  17556  acsfn  17557  lubeldm  18249  lubval  18252  glbeldm  18262  glbval  18265  clatlem  18400  clatlubcl2  18402  clatglbcl2  18404  issubmgm  18602  issubm  18703  issubg  19031  cntzval  19226  sylow1lem2  19504  lsmvalx  19544  pj1fval  19599  issubrng  20455  issubrg  20479  rgspnval  20520  islss  20860  lspval  20901  lspcl  20902  islbs  21003  lbsextlem1  21088  lbsextlem3  21090  lbsextlem4  21091  sraval  21102  ocvval  21597  isobs  21650  islinds  21739  aspval  21803  uncmp  23311  cmpfi  23316  cmpfii  23317  2ndc1stc  23359  1stcrest  23361  hausllycmp  23402  lly1stc  23404  1stckgenlem  23461  txlly  23544  txnlly  23545  tx1stc  23558  basqtop  23619  tgqtop  23620  alexsubALTlem3  23957  alexsubALTlem4  23958  alexsubALT  23959  cncfval  24801  cnllycmp  24875  ovolficcss  25390  ovolval  25394  ovolicc2  25443  ismbl  25447  mblsplit  25453  voliunlem3  25473  vitalilem4  25532  vitalilem5  25533  dvfval  25818  dvnfval  25844  cpnfval  25854  plyval  26118  dmarea  26887  wilthlem2  26999  issh  31178  ocval  31250  spanval  31303  hsupval  31304  sshjval  31320  sshjval3  31324  zarcls  33877  zartopn  33878  sigagensiga  34144  dya2iocuni  34286  coinflippv  34487  ballotlemelo  34491  ballotth  34541  erdszelem1  35203  kur14lem9  35226  kur14  35228  cnllysconn  35257  elmpst  35548  mclsrcl  35573  mclsval  35575  icoreresf  37365  cntotbnd  37815  heibor1lem  37828  heibor  37840  isidl  38033  igenval  38080  paddval  39816  pclvalN  39908  polvalN  39923  docavalN  41141  djavalN  41153  dicval  41194  dochval  41369  djhval  41416  lpolconN  41505  elpwbi  42242  elmzpcl  42738  eldiophb  42769  rpnnen3  43044  islssfgi  43084  hbt  43142  elmnc  43148  itgoval  43173  itgocn  43176  elpglem2  49723