Theorem elpw2 5274

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4551

This theorem is referenced by:  elpwi2  5275  axpweq  5291  knatar  7297  dffi3  9321  marypha1lem  9323  r1pwss  9683  rankr1bg  9702  pwwf  9706  unwf  9709  rankval2  9717  uniwf  9718  rankpwi  9722  dfac2a  10027  dfac12lem2  10042  axdc4lem  10352  axdclem  10416  incexclem  15749  rpnnen2lem1  16129  rpnnen2lem2  16130  sadfval  16369  smufval  16394  smupf  16395  vdwapf  16890  prdshom  17377  mreacs  17570  acsfn  17571  lubeldm  18263  lubval  18266  glbeldm  18276  glbval  18279  clatlem  18414  clatlubcl2  18416  clatglbcl2  18418  issubmgm  18616  issubm  18717  issubg  19045  cntzval  19239  sylow1lem2  19517  lsmvalx  19557  pj1fval  19612  issubrng  20468  issubrg  20492  rgspnval  20533  islss  20873  lspval  20914  lspcl  20915  islbs  21016  lbsextlem1  21101  lbsextlem3  21103  lbsextlem4  21104  sraval  21115  ocvval  21610  isobs  21663  islinds  21752  aspval  21816  uncmp  23324  cmpfi  23329  cmpfii  23330  2ndc1stc  23372  1stcrest  23374  hausllycmp  23415  lly1stc  23417  1stckgenlem  23474  txlly  23557  txnlly  23558  tx1stc  23571  basqtop  23632  tgqtop  23633  alexsubALTlem3  23970  alexsubALTlem4  23971  alexsubALT  23972  cncfval  24814  cnllycmp  24888  ovolficcss  25403  ovolval  25407  ovolicc2  25456  ismbl  25460  mblsplit  25466  voliunlem3  25486  vitalilem4  25545  vitalilem5  25546  dvfval  25831  dvnfval  25857  cpnfval  25867  plyval  26131  dmarea  26900  wilthlem2  27012  issh  31195  ocval  31267  spanval  31320  hsupval  31321  sshjval  31337  sshjval3  31341  zarcls  33894  zartopn  33895  sigagensiga  34161  dya2iocuni  34303  coinflippv  34504  ballotlemelo  34508  ballotth  34558  rankval2b  35117  r1ssel  35125  erdszelem1  35242  kur14lem9  35265  kur14  35267  cnllysconn  35296  elmpst  35587  mclsrcl  35612  mclsval  35614  icoreresf  37403  cntotbnd  37842  heibor1lem  37855  heibor  37867  isidl  38060  igenval  38107  paddval  39903  pclvalN  39995  polvalN  40010  docavalN  41228  djavalN  41240  dicval  41281  dochval  41456  djhval  41503  lpolconN  41592  elpwbi  42329  elmzpcl  42824  eldiophb  42855  rpnnen3  43130  islssfgi  43170  hbt  43228  elmnc  43234  itgoval  43259  itgocn  43262  elpglem2  49818