Theorem elpw2 5304

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926  𝒫 cpw 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  elpwi2  5305  axpweq  5321  knatar  7350  dffi3  9443  marypha1lem  9445  r1pwss  9798  rankr1bg  9817  pwwf  9821  unwf  9824  rankval2  9832  uniwf  9833  rankpwi  9837  dfac2a  10144  dfac12lem2  10159  axdc4lem  10469  axdclem  10533  incexclem  15852  rpnnen2lem1  16232  rpnnen2lem2  16233  sadfval  16471  smufval  16496  smupf  16497  vdwapf  16992  prdshom  17481  mreacs  17670  acsfn  17671  lubeldm  18363  lubval  18366  glbeldm  18376  glbval  18379  clatlem  18512  clatlubcl2  18514  clatglbcl2  18516  issubmgm  18680  issubm  18781  issubg  19109  cntzval  19304  sylow1lem2  19580  lsmvalx  19620  pj1fval  19675  issubrng  20507  issubrg  20531  rgspnval  20572  islss  20891  lspval  20932  lspcl  20933  islbs  21034  lbsextlem1  21119  lbsextlem3  21121  lbsextlem4  21122  sraval  21133  ocvval  21627  isobs  21680  islinds  21769  aspval  21833  uncmp  23341  cmpfi  23346  cmpfii  23347  2ndc1stc  23389  1stcrest  23391  hausllycmp  23432  lly1stc  23434  1stckgenlem  23491  txlly  23574  txnlly  23575  tx1stc  23588  basqtop  23649  tgqtop  23650  alexsubALTlem3  23987  alexsubALTlem4  23988  alexsubALT  23989  cncfval  24832  cnllycmp  24906  ovolficcss  25422  ovolval  25426  ovolicc2  25475  ismbl  25479  mblsplit  25485  voliunlem3  25505  vitalilem4  25564  vitalilem5  25565  dvfval  25850  dvnfval  25876  cpnfval  25886  plyval  26150  dmarea  26919  wilthlem2  27031  issh  31189  ocval  31261  spanval  31314  hsupval  31315  sshjval  31331  sshjval3  31335  zarcls  33905  zartopn  33906  sigagensiga  34172  dya2iocuni  34315  coinflippv  34516  ballotlemelo  34520  ballotth  34570  erdszelem1  35213  kur14lem9  35236  kur14  35238  cnllysconn  35267  elmpst  35558  mclsrcl  35583  mclsval  35585  icoreresf  37370  cntotbnd  37820  heibor1lem  37833  heibor  37845  isidl  38038  igenval  38085  paddval  39817  pclvalN  39909  polvalN  39924  docavalN  41142  djavalN  41154  dicval  41195  dochval  41370  djhval  41417  lpolconN  41506  elpwbi  42281  elmzpcl  42749  eldiophb  42780  rpnnen3  43056  islssfgi  43096  hbt  43154  elmnc  43160  itgoval  43185  itgocn  43188  elpglem2  49576