Theorem sselpwd 5272

Description: Elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)

Hypotheses

Ref	Expression
sselpwd.1	⊢ (𝜑 → 𝐵 ∈ 𝑉)
sselpwd.2	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
sselpwd	⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Proof of Theorem sselpwd

Step	Hyp	Ref	Expression
1		sselpwd.1	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
2		sselpwd.2	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	1, 2	ssexd 5268	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
4	3, 2	elpwd 4559	1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3439   ⊆ wss 3900  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-in 3907  df-ss 3917  df-pw 4555

This theorem is referenced by:  knatar  7303  marypha1  9339  fin1a2lem7  10318  canthp1lem2  10566  wunss  10625  ramub1lem1  16956  mreexd  17567  mreexexlemd  17569  mreexexlem4d  17572  opsrval  22003  selvfval  22079  cncls  23220  fbasrn  23830  rnelfmlem  23898  ustssel  24152  hashimaf1  32870  pwrssmgc  33061  esplyfv1  33706  exsslsb  33732  crefi  33983  ldsysgenld  34296  ldgenpisyslem1  34299  bj-ismoored  37281  bj-imdirval2  37357  bj-iminvval2  37368  sticksstones2  42436  rfovcnvf1od  44282  fsovrfovd  44287  fsovfd  44290  fsovcnvlem  44291  ntrclsrcomplex  44313  clsk3nimkb  44318  clsk1indlem4  44322  clsk1indlem1  44323  ntrclsiso  44345  ntrclskb  44347  ntrclsk3  44348  ntrclsk13  44349  ntrneircomplex  44352  ntrneik3  44374  ntrneix3  44375  ntrneik13  44376  ntrneix13  44377  clsneircomplex  44381  clsneiel1  44386  neicvgrcomplex  44391  neicvgel1  44397  mnussd  44541  mnuprssd  44547  mnuop3d  44549  wessf1ornlem  45466  dvnprodlem1  46227  ovolsplit  46269  saliunclf  46603  sge0f1o  46663  isisubgr  48145  iscnrm3rlem3  49224