Theorem elpw2 5264

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3427   ⊆ wss 3885  𝒫 cpw 4531

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 2707  ax-sep 5220

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 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-in 3892  df-ss 3902  df-pw 4533

This theorem is referenced by:  elpwi2  5265  axpweq  5281  knatar  7301  dffi3  9333  marypha1lem  9335  r1pwss  9697  rankr1bg  9716  pwwf  9720  unwf  9723  rankval2  9731  uniwf  9732  rankpwi  9736  dfac2a  10041  dfac12lem2  10056  axdc4lem  10366  axdclem  10430  incexclem  15790  rpnnen2lem1  16170  rpnnen2lem2  16171  sadfval  16410  smufval  16435  smupf  16436  vdwapf  16932  prdshom  17419  mreacs  17613  acsfn  17614  lubeldm  18306  lubval  18309  glbeldm  18319  glbval  18322  clatlem  18457  clatlubcl2  18459  clatglbcl2  18461  issubmgm  18659  issubm  18760  issubg  19091  cntzval  19285  sylow1lem2  19563  lsmvalx  19603  pj1fval  19658  issubrng  20513  issubrg  20537  rgspnval  20578  islss  20918  lspval  20959  lspcl  20960  islbs  21060  lbsextlem1  21145  lbsextlem3  21147  lbsextlem4  21148  sraval  21159  ocvval  21636  isobs  21689  islinds  21778  aspval  21841  uncmp  23356  cmpfi  23361  cmpfii  23362  2ndc1stc  23404  1stcrest  23406  hausllycmp  23447  lly1stc  23449  1stckgenlem  23506  txlly  23589  txnlly  23590  tx1stc  23603  basqtop  23664  tgqtop  23665  alexsubALTlem3  24002  alexsubALTlem4  24003  alexsubALT  24004  cncfval  24843  cnllycmp  24911  ovolficcss  25424  ovolval  25428  ovolicc2  25477  ismbl  25481  mblsplit  25487  voliunlem3  25507  vitalilem4  25566  vitalilem5  25567  dvfval  25852  dvnfval  25877  cpnfval  25887  plyval  26146  dmarea  26909  wilthlem2  27020  issh  31267  ocval  31339  spanval  31392  hsupval  31393  sshjval  31409  sshjval3  31413  zarcls  34006  zartopn  34007  sigagensiga  34273  dya2iocuni  34415  coinflippv  34616  ballotlemelo  34620  ballotth  34670  rankval2b  35230  r1ssel  35238  erdszelem1  35361  kur14lem9  35384  kur14  35386  cnllysconn  35415  elmpst  35706  mclsrcl  35731  mclsval  35733  ttcwf  36694  icoreresf  37656  cntotbnd  38105  heibor1lem  38118  heibor  38130  isidl  38323  igenval  38370  paddval  40232  pclvalN  40324  polvalN  40339  docavalN  41557  djavalN  41569  dicval  41610  dochval  41785  djhval  41832  lpolconN  41921  elpwbi  42659  elmzpcl  43146  eldiophb  43177  rpnnen3  43448  islssfgi  43488  hbt  43546  elmnc  43552  itgoval  43577  itgocn  43580  elpglem2  50175