Theorem sselpwd 5204

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

Syntax hints:   → wi 4   ∈ wcel 2112  Vcvv 3398   ⊆ wss 3853  𝒫 cpw 4499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870  df-pw 4501

This theorem is referenced by:  knatar  7144  marypha1  9028  fin1a2lem7  9985  canthp1lem2  10232  wunss  10291  ramub1lem1  16542  mreexd  17099  mreexexlemd  17101  mreexexlem4d  17104  opsrval  20957  selvfval  21031  cncls  22125  fbasrn  22735  rnelfmlem  22803  ustssel  23057  pwrssmgc  30951  crefi  31465  ldsysgenld  31794  ldgenpisyslem1  31797  bj-ismoored  34962  bj-imdirval2  35038  bj-iminvval2  35049  sticksstones2  39772  rfovcnvf1od  41230  fsovrfovd  41235  fsovfd  41238  fsovcnvlem  41239  ntrclsrcomplex  41263  clsk3nimkb  41268  clsk1indlem4  41272  clsk1indlem1  41273  ntrclsiso  41295  ntrclskb  41297  ntrclsk3  41298  ntrclsk13  41299  ntrneircomplex  41302  ntrneik3  41324  ntrneix3  41325  ntrneik13  41326  ntrneix13  41327  clsneircomplex  41331  clsneiel1  41336  neicvgrcomplex  41341  neicvgel1  41347  mnussd  41495  mnuprssd  41501  mnuop3d  41503  wessf1ornlem  42336  ovolsplit  43147  iscnrm3rlem3  45852