Theorem elpw2 5291

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3916  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3923  df-ss 3933  df-pw 4567

This theorem is referenced by:  elpwi2  5292  axpweq  5308  knatar  7334  dffi3  9388  marypha1lem  9390  r1pwss  9743  rankr1bg  9762  pwwf  9766  unwf  9769  rankval2  9777  uniwf  9778  rankpwi  9782  dfac2a  10089  dfac12lem2  10104  axdc4lem  10414  axdclem  10478  incexclem  15808  rpnnen2lem1  16188  rpnnen2lem2  16189  sadfval  16428  smufval  16453  smupf  16454  vdwapf  16949  prdshom  17436  mreacs  17625  acsfn  17626  lubeldm  18318  lubval  18321  glbeldm  18331  glbval  18334  clatlem  18467  clatlubcl2  18469  clatglbcl2  18471  issubmgm  18635  issubm  18736  issubg  19064  cntzval  19259  sylow1lem2  19535  lsmvalx  19575  pj1fval  19630  issubrng  20462  issubrg  20486  rgspnval  20527  islss  20846  lspval  20887  lspcl  20888  islbs  20989  lbsextlem1  21074  lbsextlem3  21076  lbsextlem4  21077  sraval  21088  ocvval  21582  isobs  21635  islinds  21724  aspval  21788  uncmp  23296  cmpfi  23301  cmpfii  23302  2ndc1stc  23344  1stcrest  23346  hausllycmp  23387  lly1stc  23389  1stckgenlem  23446  txlly  23529  txnlly  23530  tx1stc  23543  basqtop  23604  tgqtop  23605  alexsubALTlem3  23942  alexsubALTlem4  23943  alexsubALT  23944  cncfval  24787  cnllycmp  24861  ovolficcss  25376  ovolval  25380  ovolicc2  25429  ismbl  25433  mblsplit  25439  voliunlem3  25459  vitalilem4  25518  vitalilem5  25519  dvfval  25804  dvnfval  25830  cpnfval  25840  plyval  26104  dmarea  26873  wilthlem2  26985  issh  31143  ocval  31215  spanval  31268  hsupval  31269  sshjval  31285  sshjval3  31289  zarcls  33870  zartopn  33871  sigagensiga  34137  dya2iocuni  34280  coinflippv  34481  ballotlemelo  34485  ballotth  34535  erdszelem1  35178  kur14lem9  35201  kur14  35203  cnllysconn  35232  elmpst  35523  mclsrcl  35548  mclsval  35550  icoreresf  37335  cntotbnd  37785  heibor1lem  37798  heibor  37810  isidl  38003  igenval  38050  paddval  39787  pclvalN  39879  polvalN  39894  docavalN  41112  djavalN  41124  dicval  41165  dochval  41340  djhval  41387  lpolconN  41476  elpwbi  42213  elmzpcl  42707  eldiophb  42738  rpnnen3  43014  islssfgi  43054  hbt  43112  elmnc  43118  itgoval  43143  itgocn  43146  elpglem2  49691