Theorem elpw2 5346

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949  𝒫 cpw 4603

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 5300

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 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  elpwi2  5347  axpweq  5349  knatar  7354  dffi3  9426  marypha1lem  9428  r1pwss  9779  rankr1bg  9798  pwwf  9802  unwf  9805  rankval2  9813  uniwf  9814  rankpwi  9818  dfac2a  10124  dfac12lem2  10139  axdc4lem  10450  axdclem  10514  incexclem  15782  rpnnen2lem1  16157  rpnnen2lem2  16158  sadfval  16393  smufval  16418  smupf  16419  vdwapf  16905  prdshom  17413  mreacs  17602  acsfn  17603  lubeldm  18306  lubval  18309  glbeldm  18319  glbval  18322  clatlem  18455  clatlubcl2  18457  clatglbcl2  18459  issubm  18684  issubg  19006  cntzval  19185  sylow1lem2  19467  lsmvalx  19507  pj1fval  19562  issubrg  20319  islss  20545  lspval  20586  lspcl  20587  islbs  20687  lbsextlem1  20771  lbsextlem3  20773  lbsextlem4  20774  sraval  20789  ocvval  21220  isobs  21275  islinds  21364  aspval  21427  uncmp  22907  cmpfi  22912  cmpfii  22913  2ndc1stc  22955  1stcrest  22957  hausllycmp  22998  lly1stc  23000  1stckgenlem  23057  txlly  23140  txnlly  23141  tx1stc  23154  basqtop  23215  tgqtop  23216  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  cncfval  24404  cnllycmp  24472  ovolficcss  24986  ovolval  24990  ovolicc2  25039  ismbl  25043  mblsplit  25049  voliunlem3  25069  vitalilem4  25128  vitalilem5  25129  dvfval  25414  dvnfval  25439  cpnfval  25449  plyval  25707  dmarea  26462  wilthlem2  26573  issh  30461  ocval  30533  spanval  30586  hsupval  30587  sshjval  30603  sshjval3  30607  zarcls  32854  zartopn  32855  sigagensiga  33139  dya2iocuni  33282  coinflippv  33482  ballotlemelo  33486  ballotth  33536  erdszelem1  34182  kur14lem9  34205  kur14  34207  cnllysconn  34236  elmpst  34527  mclsrcl  34552  mclsval  34554  icoreresf  36233  cntotbnd  36664  heibor1lem  36677  heibor  36689  isidl  36882  igenval  36929  paddval  38669  pclvalN  38761  polvalN  38776  docavalN  39994  djavalN  40006  dicval  40047  dochval  40222  djhval  40269  lpolconN  40358  elpwbi  41049  elmzpcl  41464  eldiophb  41495  rpnnen3  41771  islssfgi  41814  hbt  41872  elmnc  41878  itgoval  41903  itgocn  41906  rgspnval  41910  issubmgm  46559  issubrng  46726  elpglem2  47757