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 205   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  elpwi2  5265  axpweq  5282  knatar  7208  dffi3  9120  marypha1lem  9122  r1pwss  9473  rankr1bg  9492  pwwf  9496  unwf  9499  rankval2  9507  uniwf  9508  rankpwi  9512  dfac2a  9816  dfac12lem2  9831  axdc4lem  10142  axdclem  10206  incexclem  15476  rpnnen2lem1  15851  rpnnen2lem2  15852  sadfval  16087  smufval  16112  smupf  16113  vdwapf  16601  prdshom  17095  mreacs  17284  acsfn  17285  lubeldm  17986  lubval  17989  glbeldm  17999  glbval  18002  clatlem  18135  clatlubcl2  18137  clatglbcl2  18139  issubm  18357  issubg  18670  cntzval  18842  sylow1lem2  19119  lsmvalx  19159  pj1fval  19215  issubrg  19939  islss  20111  lspval  20152  lspcl  20153  islbs  20253  lbsextlem1  20335  lbsextlem3  20337  lbsextlem4  20338  sraval  20353  ocvval  20784  isobs  20837  islinds  20926  aspval  20987  uncmp  22462  cmpfi  22467  cmpfii  22468  2ndc1stc  22510  1stcrest  22512  hausllycmp  22553  lly1stc  22555  1stckgenlem  22612  txlly  22695  txnlly  22696  tx1stc  22709  basqtop  22770  tgqtop  22771  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  cncfval  23957  cnllycmp  24025  ovolficcss  24538  ovolval  24542  ovolicc2  24591  ismbl  24595  mblsplit  24601  voliunlem3  24621  vitalilem4  24680  vitalilem5  24681  dvfval  24966  dvnfval  24991  cpnfval  25001  plyval  25259  dmarea  26012  wilthlem2  26123  issh  29471  ocval  29543  spanval  29596  hsupval  29597  sshjval  29613  sshjval3  29617  zarcls  31726  zartopn  31727  sigagensiga  32009  dya2iocuni  32150  coinflippv  32350  ballotlemelo  32354  ballotth  32404  erdszelem1  33053  kur14lem9  33076  kur14  33078  cnllysconn  33107  elmpst  33398  mclsrcl  33423  mclsval  33425  icoreresf  35450  cntotbnd  35881  heibor1lem  35894  heibor  35906  isidl  36099  igenval  36146  paddval  37739  pclvalN  37831  polvalN  37846  docavalN  39064  djavalN  39076  dicval  39117  dochval  39292  djhval  39339  lpolconN  39428  elpwbi  40131  elmzpcl  40464  eldiophb  40495  rpnnen3  40770  islssfgi  40813  hbt  40871  elmnc  40877  itgoval  40902  itgocn  40905  rgspnval  40909  issubmgm  45231  elpglem2  46303