Theorem elpw2 5344

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3947  𝒫 cpw 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3954  df-ss 3964  df-pw 4603

This theorem is referenced by:  elpwi2  5345  axpweq  5347  knatar  7349  dffi3  9422  marypha1lem  9424  r1pwss  9775  rankr1bg  9794  pwwf  9798  unwf  9801  rankval2  9809  uniwf  9810  rankpwi  9814  dfac2a  10120  dfac12lem2  10135  axdc4lem  10446  axdclem  10510  incexclem  15778  rpnnen2lem1  16153  rpnnen2lem2  16154  sadfval  16389  smufval  16414  smupf  16415  vdwapf  16901  prdshom  17409  mreacs  17598  acsfn  17599  lubeldm  18302  lubval  18305  glbeldm  18315  glbval  18318  clatlem  18451  clatlubcl2  18453  clatglbcl2  18455  issubm  18680  issubg  19000  cntzval  19179  sylow1lem2  19460  lsmvalx  19500  pj1fval  19555  issubrg  20351  islss  20533  lspval  20574  lspcl  20575  islbs  20675  lbsextlem1  20759  lbsextlem3  20761  lbsextlem4  20762  sraval  20777  ocvval  21204  isobs  21259  islinds  21348  aspval  21409  uncmp  22889  cmpfi  22894  cmpfii  22895  2ndc1stc  22937  1stcrest  22939  hausllycmp  22980  lly1stc  22982  1stckgenlem  23039  txlly  23122  txnlly  23123  tx1stc  23136  basqtop  23197  tgqtop  23198  alexsubALTlem3  23535  alexsubALTlem4  23536  alexsubALT  23537  cncfval  24386  cnllycmp  24454  ovolficcss  24968  ovolval  24972  ovolicc2  25021  ismbl  25025  mblsplit  25031  voliunlem3  25051  vitalilem4  25110  vitalilem5  25111  dvfval  25396  dvnfval  25421  cpnfval  25431  plyval  25689  dmarea  26442  wilthlem2  26553  issh  30439  ocval  30511  spanval  30564  hsupval  30565  sshjval  30581  sshjval3  30585  zarcls  32792  zartopn  32793  sigagensiga  33077  dya2iocuni  33220  coinflippv  33420  ballotlemelo  33424  ballotth  33474  erdszelem1  34120  kur14lem9  34143  kur14  34145  cnllysconn  34174  elmpst  34465  mclsrcl  34490  mclsval  34492  icoreresf  36171  cntotbnd  36602  heibor1lem  36615  heibor  36627  isidl  36820  igenval  36867  paddval  38607  pclvalN  38699  polvalN  38714  docavalN  39932  djavalN  39944  dicval  39985  dochval  40160  djhval  40207  lpolconN  40296  elpwbi  40997  elmzpcl  41397  eldiophb  41428  rpnnen3  41704  islssfgi  41747  hbt  41805  elmnc  41811  itgoval  41836  itgocn  41839  rgspnval  41843  issubmgm  46494  issubrng  46659  elpglem2  47659