Theorem sselpwd 5245

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  knatar  7208  marypha1  9123  fin1a2lem7  10093  canthp1lem2  10340  wunss  10399  ramub1lem1  16655  mreexd  17268  mreexexlemd  17270  mreexexlem4d  17273  opsrval  21157  selvfval  21237  cncls  22333  fbasrn  22943  rnelfmlem  23011  ustssel  23265  pwrssmgc  31180  crefi  31699  ldsysgenld  32028  ldgenpisyslem1  32031  bj-ismoored  35205  bj-imdirval2  35281  bj-iminvval2  35292  sticksstones2  40031  rfovcnvf1od  41501  fsovrfovd  41506  fsovfd  41509  fsovcnvlem  41510  ntrclsrcomplex  41534  clsk3nimkb  41539  clsk1indlem4  41543  clsk1indlem1  41544  ntrclsiso  41566  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  ntrneircomplex  41573  ntrneik3  41595  ntrneix3  41596  ntrneik13  41597  ntrneix13  41598  clsneircomplex  41602  clsneiel1  41607  neicvgrcomplex  41612  neicvgel1  41618  mnussd  41770  mnuprssd  41776  mnuop3d  41778  wessf1ornlem  42611  ovolsplit  43419  iscnrm3rlem3  46124