Theorem elpw2 5334

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951  𝒫 cpw 4600

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 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  elpwi2  5335  axpweq  5351  knatar  7377  dffi3  9471  marypha1lem  9473  r1pwss  9824  rankr1bg  9843  pwwf  9847  unwf  9850  rankval2  9858  uniwf  9859  rankpwi  9863  dfac2a  10170  dfac12lem2  10185  axdc4lem  10495  axdclem  10559  incexclem  15872  rpnnen2lem1  16250  rpnnen2lem2  16251  sadfval  16489  smufval  16514  smupf  16515  vdwapf  17010  prdshom  17512  mreacs  17701  acsfn  17702  lubeldm  18398  lubval  18401  glbeldm  18411  glbval  18414  clatlem  18547  clatlubcl2  18549  clatglbcl2  18551  issubmgm  18715  issubm  18816  issubg  19144  cntzval  19339  sylow1lem2  19617  lsmvalx  19657  pj1fval  19712  issubrng  20547  issubrg  20571  rgspnval  20612  islss  20932  lspval  20973  lspcl  20974  islbs  21075  lbsextlem1  21160  lbsextlem3  21162  lbsextlem4  21163  sraval  21174  ocvval  21685  isobs  21740  islinds  21829  aspval  21893  uncmp  23411  cmpfi  23416  cmpfii  23417  2ndc1stc  23459  1stcrest  23461  hausllycmp  23502  lly1stc  23504  1stckgenlem  23561  txlly  23644  txnlly  23645  tx1stc  23658  basqtop  23719  tgqtop  23720  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  cncfval  24914  cnllycmp  24988  ovolficcss  25504  ovolval  25508  ovolicc2  25557  ismbl  25561  mblsplit  25567  voliunlem3  25587  vitalilem4  25646  vitalilem5  25647  dvfval  25932  dvnfval  25958  cpnfval  25968  plyval  26232  dmarea  27000  wilthlem2  27112  issh  31227  ocval  31299  spanval  31352  hsupval  31353  sshjval  31369  sshjval3  31373  zarcls  33873  zartopn  33874  sigagensiga  34142  dya2iocuni  34285  coinflippv  34486  ballotlemelo  34490  ballotth  34540  erdszelem1  35196  kur14lem9  35219  kur14  35221  cnllysconn  35250  elmpst  35541  mclsrcl  35566  mclsval  35568  icoreresf  37353  cntotbnd  37803  heibor1lem  37816  heibor  37828  isidl  38021  igenval  38068  paddval  39800  pclvalN  39892  polvalN  39907  docavalN  41125  djavalN  41137  dicval  41178  dochval  41353  djhval  41400  lpolconN  41489  elpwbi  42269  elmzpcl  42737  eldiophb  42768  rpnnen3  43044  islssfgi  43084  hbt  43142  elmnc  43148  itgoval  43173  itgocn  43176  elpglem2  49231