Theorem elpw2 5291

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

Syntax hints:   ↔ wb 208   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3905  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3457  df-in 3912  df-ss 3922  df-pw 4558

This theorem is referenced by:  elpwi2  5292  axpweq  5308  knatar  7341  dffi3  9375  marypha1lem  9377  r1pwss  9740  rankr1bg  9759  pwwf  9763  unwf  9766  rankval2  9774  uniwf  9775  rankpwi  9779  dfac2a  10097  dfac12lem2  10112  axdc4lem  10423  axdclem  10487  incexclem  15876  rpnnen2lem1  16256  rpnnen2lem2  16257  sadfval  16496  smufval  16521  smupf  16522  vdwapf  17018  prdshom  17506  mreacs  17700  acsfn  17701  lubeldm  18393  lubval  18396  glbeldm  18406  glbval  18409  clatlem  18544  clatlubcl2  18546  clatglbcl2  18548  issubmgm  18746  issubm  18847  issubg  19178  cntzval  19371  sylow1lem2  19649  lsmvalx  19689  pj1fval  19744  issubrng  20607  issubrg  20631  rgspnval  20672  islss  21008  lspval  21049  lspcl  21050  islbs  21150  lbsextlem1  21235  lbsextlem3  21237  lbsextlem4  21238  sraval  21249  ocvval  21726  isobs  21779  islinds  21868  aspval  21931  uncmp  23470  cmpfi  23475  cmpfii  23476  2ndc1stc  23518  1stcrest  23520  hausllycmp  23561  lly1stc  23563  1stckgenlem  23620  txlly  23703  txnlly  23704  tx1stc  23717  basqtop  23778  tgqtop  23779  alexsubALTlem3  24116  alexsubALTlem4  24117  alexsubALT  24118  cncfval  24957  cnllycmp  25025  ovolficcss  25538  ovolval  25542  ovolicc2  25591  ismbl  25595  mblsplit  25601  voliunlem3  25621  vitalilem4  25680  vitalilem5  25681  dvfval  25966  dvnfval  25991  cpnfval  26001  plyval  26260  dmarea  27029  wilthlem2  27140  issh  31418  ocval  31490  spanval  31543  hsupval  31544  sshjval  31560  sshjval3  31564  zarcls  34173  zartopn  34174  sigagensiga  34440  dya2iocuni  34582  coinflippv  34783  ballotlemelo  34787  ballotth  34837  rankval2b  35399  r1ssel  35407  erdszelem1  35546  kur14lem9  35569  kur14  35571  cnllysconn  35600  elmpst  35891  mclsrcl  35916  mclsval  35918  ttcwf  36889  icoreresf  37851  cntotbnd  38300  heibor1lem  38313  heibor  38325  isidl  38518  igenval  38565  paddval  40427  pclvalN  40519  polvalN  40534  docavalN  41752  djavalN  41764  dicval  41805  dochval  41980  djhval  42027  lpolconN  42116  elpwbi  42854  elmzpcl  43312  eldiophb  43343  rpnnen3  43614  islssfgi  43654  hbt  43712  elmnc  43718  itgoval  43743  itgocn  43746  elpglem2  50324