Theorem sselpwd 5251

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433   ⊆ wss 3888  𝒫 cpw 4534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905  df-pw 4536

This theorem is referenced by:  knatar  7237  marypha1  9202  fin1a2lem7  10171  canthp1lem2  10418  wunss  10477  ramub1lem1  16736  mreexd  17360  mreexexlemd  17362  mreexexlem4d  17365  opsrval  21256  selvfval  21336  cncls  22434  fbasrn  23044  rnelfmlem  23112  ustssel  23366  pwrssmgc  31287  crefi  31806  ldsysgenld  32137  ldgenpisyslem1  32140  bj-ismoored  35287  bj-imdirval2  35363  bj-iminvval2  35374  sticksstones2  40110  rfovcnvf1od  41619  fsovrfovd  41624  fsovfd  41627  fsovcnvlem  41628  ntrclsrcomplex  41652  clsk3nimkb  41657  clsk1indlem4  41661  clsk1indlem1  41662  ntrclsiso  41684  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  ntrneircomplex  41691  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  clsneircomplex  41720  clsneiel1  41725  neicvgrcomplex  41730  neicvgel1  41736  mnussd  41888  mnuprssd  41894  mnuop3d  41896  wessf1ornlem  42729  ovolsplit  43536  iscnrm3rlem3  46247