Theorem elpw2 5239

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

Syntax hints:   ↔ wb 208   ∈ wcel 2107  Vcvv 3493   ⊆ wss 3934  𝒫 cpw 4537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-in 3941  df-ss 3950  df-pw 4539

This theorem is referenced by:  axpweq  5256  knatar  7102  dffi3  8887  marypha1lem  8889  r1pwss  9205  rankr1bg  9224  pwwf  9228  unwf  9231  rankval2  9239  uniwf  9240  rankpwi  9244  dfac2a  9547  dfac12lem2  9562  axdc4lem  9869  axdclem  9933  incexclem  15183  rpnnen2lem1  15559  rpnnen2lem2  15560  sadfval  15793  smufval  15818  smupf  15819  vdwapf  16300  prdshom  16732  mreacs  16921  acsfn  16922  lubeldm  17583  lubval  17586  glbeldm  17596  glbval  17599  clatlem  17713  clatlubcl2  17715  clatglbcl2  17717  issubm  17960  issubg  18271  cntzval  18443  sylow1lem2  18716  lsmvalx  18756  pj1fval  18812  issubrg  19527  islss  19698  lspval  19739  lspcl  19740  islbs  19840  lbsextlem1  19922  lbsextlem3  19924  lbsextlem4  19925  sraval  19940  aspval  20094  ocvval  20803  isobs  20856  islinds  20945  uncmp  22003  cmpfi  22008  cmpfii  22009  2ndc1stc  22051  1stcrest  22053  hausllycmp  22094  lly1stc  22096  1stckgenlem  22153  txlly  22236  txnlly  22237  tx1stc  22250  basqtop  22311  tgqtop  22312  alexsubALTlem3  22649  alexsubALTlem4  22650  alexsubALT  22651  cncfval  23488  cnllycmp  23552  ovolficcss  24062  ovolval  24066  ovolicc2  24115  ismbl  24119  mblsplit  24125  voliunlem3  24145  vitalilem4  24204  vitalilem5  24205  dvfval  24487  dvnfval  24511  cpnfval  24521  plyval  24775  dmarea  25527  wilthlem2  25638  issh  28977  ocval  29049  spanval  29102  hsupval  29103  sshjval  29119  sshjval3  29123  sigagensiga  31393  dya2iocuni  31534  coinflippv  31734  ballotlemelo  31738  ballotth  31788  erdszelem1  32431  kur14lem9  32454  kur14  32456  cnllysconn  32485  elmpst  32776  mclsrcl  32801  mclsval  32803  icoreresf  34625  cntotbnd  35066  heibor1lem  35079  heibor  35091  isidl  35284  igenval  35331  paddval  36926  pclvalN  37018  polvalN  37033  docavalN  38251  djavalN  38263  dicval  38304  dochval  38479  djhval  38526  lpolconN  38615  elpwbi  39106  elmzpcl  39313  eldiophb  39344  rpnnen3  39619  islssfgi  39662  hbt  39720  elmnc  39726  itgoval  39751  itgocn  39754  rgspnval  39758  issubmgm  44046  elpglem2  44804