Theorem elpw2 5303

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-pw 4562

This theorem is used by:  elpwi2  5304  axpweq  5319  knatar  7363  dffi3  9404  marypha1lem  9406  r1pwss  9769  rankr1bg  9788  pwwf  9792  unwf  9795  rankval2  9803  uniwf  9804  rankpwi  9808  dfac2a  10135  dfac12lem2  10150  axdc4lem  10460  axdclem  10524  incexclem  15927  rpnnen2lem1  16306  rpnnen2lem2  16307  sadfval  16546  smufval  16571  smupf  16572  vdwapf  17068  prdshom  17556  mreacs  17750  acsfn  17751  lubeldm  18443  lubval  18446  glbeldm  18456  glbval  18459  clatlem  18594  clatlubcl2  18596  clatglbcl2  18598  issubmgm  18806  issubm  18912  issubg  19250  cntzval  19449  sylow1lem2  19727  lsmvalx  19767  pj1fval  19822  issubrng  20710  issubrg  20734  rgspnval  20775  islss  21119  lspval  21160  lspcl  21161  islbs  21261  lbsextlem1  21346  lbsextlem3  21348  lbsextlem4  21349  sraval  21360  ocvval  21881  isobs  21934  islinds  22023  aspval  22088  uncmp  23629  cmpfi  23634  cmpfii  23635  2ndc1stc  23677  1stcrest  23679  hausllycmp  23721  lly1stc  23723  1stckgenlem  23780  txlly  23863  txnlly  23864  tx1stc  23877  basqtop  23938  tgqtop  23939  alexsubALTlem3  24276  alexsubALTlem4  24277  alexsubALT  24278  cncfval  25117  cnllycmp  25185  ovolficcss  25698  ovolval  25702  ovolicc2  25751  ismbl  25755  mblsplit  25761  voliunlem3  25781  vitalilem4  25840  vitalilem5  25841  dvfval  26126  dvnfval  26151  cpnfval  26161  plyval  26420  dmarea  27192  wilthlem2  27303  issh  31675  ocval  31747  spanval  31800  hsupval  31801  sshjval  31817  sshjval3  31821  zarcls  34371  zartopn  34372  sigagensiga  34639  dya2iocuni  34781  coinflippv  34982  ballotlemelo  34986  ballotth  35036  rankval2b  35593  r1ssel  35602  erdszelem1  35757  kur14lem9  35780  kur14  35782  cnllysconn  35811  elmpst  36102  mclsrcl  36127  mclsval  36129  ttcwf  37130  icoreresf  38093  cntotbnd  38533  heibor1lem  38546  heibor  38558  isidl  38751  igenval  38798  paddval  40658  pclvalN  40750  polvalN  40765  docavalN  41983  djavalN  41995  dicval  42036  dochval  42211  djhval  42258  lpolconN  42347  elpwbi  43087  elmzpcl  43558  eldiophb  43589  rpnnen3  43860  islssfgi  43900  hbt  43958  elmnc  43964  itgoval  43989  itgocn  43992  elpglem2  50625