Theorem sselpwd 5326

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 5324	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
4	3, 2	elpwd 4608	1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3948  𝒫 cpw 4602

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  knatar  7356  marypha1  9431  fin1a2lem7  10403  canthp1lem2  10650  wunss  10709  ramub1lem1  16963  mreexd  17590  mreexexlemd  17592  mreexexlem4d  17595  opsrval  21820  selvfval  21899  cncls  22998  fbasrn  23608  rnelfmlem  23676  ustssel  23930  pwrssmgc  32425  crefi  33113  ldsysgenld  33444  ldgenpisyslem1  33447  bj-ismoored  36291  bj-imdirval2  36367  bj-iminvval2  36378  sticksstones2  41269  rfovcnvf1od  43057  fsovrfovd  43062  fsovfd  43065  fsovcnvlem  43066  ntrclsrcomplex  43088  clsk3nimkb  43093  clsk1indlem4  43097  clsk1indlem1  43098  ntrclsiso  43120  ntrclskb  43122  ntrclsk3  43123  ntrclsk13  43124  ntrneircomplex  43127  ntrneik3  43149  ntrneix3  43150  ntrneik13  43151  ntrneix13  43152  clsneircomplex  43156  clsneiel1  43161  neicvgrcomplex  43166  neicvgel1  43172  mnussd  43324  mnuprssd  43330  mnuop3d  43332  wessf1ornlem  44183  ovolsplit  45003  saliunclf  45337  iscnrm3rlem3  47663