Theorem sselpwd 5333

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979  df-pw 4606

This theorem is referenced by:  knatar  7376  marypha1  9471  fin1a2lem7  10443  canthp1lem2  10690  wunss  10749  ramub1lem1  17059  mreexd  17686  mreexexlemd  17688  mreexexlem4d  17691  opsrval  22081  selvfval  22155  cncls  23297  fbasrn  23907  rnelfmlem  23975  ustssel  24229  pwrssmgc  32974  crefi  33807  ldsysgenld  34140  ldgenpisyslem1  34143  bj-ismoored  37089  bj-imdirval2  37165  bj-iminvval2  37176  sticksstones2  42128  rfovcnvf1od  43993  fsovrfovd  43998  fsovfd  44001  fsovcnvlem  44002  ntrclsrcomplex  44024  clsk3nimkb  44029  clsk1indlem4  44033  clsk1indlem1  44034  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrneircomplex  44063  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  clsneircomplex  44092  clsneiel1  44097  neicvgrcomplex  44102  neicvgel1  44108  mnussd  44258  mnuprssd  44264  mnuop3d  44266  wessf1ornlem  45127  dvnprodlem1  45901  ovolsplit  45943  saliunclf  46277  sge0f1o  46337  isisubgr  47785  iscnrm3rlem3  48738