Theorem elpw2 5300

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-pw 4562

This theorem is used by:  elpwi2  5301  axpweq  5316  knatar  7390  dffi3  9450  marypha1lem  9452  r1pwss  9818  rankr1bg  9838  pwwf  9842  unwf  9845  rankval2  9854  uniwf  9855  rankpwi  9859  rankval2b  9862  dfac2a  10235  dfac12lem2  10250  axdc4lem  10560  axdclem  10624  incexclem  16034  rpnnen2lem1  16411  rpnnen2lem2  16412  sadfval  16651  smufval  16676  smupf  16677  vdwapf  17179  prdshom  17667  mreacs  17861  acsfn  17862  lubeldm  18554  lubval  18557  glbeldm  18567  glbval  18570  clatlem  18705  clatlubcl2  18707  clatglbcl2  18709  issubmgm  18920  issubm  19027  issubg  19365  cntzval  19565  sylow1lem2  19843  lsmvalx  19883  pj1fval  19938  issubrng  20829  issubrg  20853  rgspnval  20894  islss  21239  lspval  21280  lspcl  21281  islbs  21381  lbsextlem1  21466  lbsextlem3  21468  lbsextlem4  21469  sraval  21480  ocvval  22003  isobs  22056  islinds  22145  aspval  22210  uncmp  23751  cmpfi  23756  cmpfii  23757  2ndc1stc  23799  1stcrest  23801  hausllycmp  23843  lly1stc  23845  1stckgenlem  23902  txlly  23985  txnlly  23986  tx1stc  23999  basqtop  24060  tgqtop  24061  alexsubALTlem3  24398  alexsubALTlem4  24399  alexsubALT  24400  cncfval  25239  cnllycmp  25307  ovolficcss  25820  ovolval  25824  ovolicc2  25873  ismbl  25877  mblsplit  25883  voliunlem3  25903  vitalilem4  25962  vitalilem5  25963  dvfval  26247  dvnfval  26272  cpnfval  26282  plyval  26541  dmarea  27315  wilthlem2  27426  issh  31840  ocval  31912  spanval  31965  hsupval  31966  sshjval  31982  sshjval3  31986  zarcls  34576  zartopn  34577  sigagensiga  34844  dya2iocuni  34985  coinflippv  35186  ballotlemelo  35190  ballotth  35240  r1ssel  35814  erdszelem1  36123  kur14lem9  36146  kur14  36148  cnllysconn  36177  elmpst  36468  mclsrcl  36493  mclsval  36495  ttcwf  37490  icoreresf  38467  cntotbnd  38922  heibor1lem  38935  heibor  38947  isidl  39140  igenval  39187  paddval  41047  pclvalN  41139  polvalN  41154  docavalN  42372  djavalN  42384  dicval  42425  dochval  42600  djhval  42647  lpolconN  42736  elpwbi  43477  elmzpcl  43930  eldiophb  43961  rpnnen3  44232  islssfgi  44267  hbt  44324  elmnc  44330  itgoval  44355  itgocn  44358  elpglem2  51085