Theorem sselpwd 5328

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 4606	1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951  𝒫 cpw 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  knatar  7377  marypha1  9474  fin1a2lem7  10446  canthp1lem2  10693  wunss  10752  ramub1lem1  17064  mreexd  17685  mreexexlemd  17687  mreexexlem4d  17690  opsrval  22064  selvfval  22138  cncls  23282  fbasrn  23892  rnelfmlem  23960  ustssel  24214  pwrssmgc  32990  exsslsb  33647  crefi  33846  ldsysgenld  34161  ldgenpisyslem1  34164  bj-ismoored  37108  bj-imdirval2  37184  bj-iminvval2  37195  sticksstones2  42148  rfovcnvf1od  44017  fsovrfovd  44022  fsovfd  44025  fsovcnvlem  44026  ntrclsrcomplex  44048  clsk3nimkb  44053  clsk1indlem4  44057  clsk1indlem1  44058  ntrclsiso  44080  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ntrneircomplex  44087  ntrneik3  44109  ntrneix3  44110  ntrneik13  44111  ntrneix13  44112  clsneircomplex  44116  clsneiel1  44121  neicvgrcomplex  44126  neicvgel1  44132  mnussd  44282  mnuprssd  44288  mnuop3d  44290  wessf1ornlem  45190  dvnprodlem1  45961  ovolsplit  46003  saliunclf  46337  sge0f1o  46397  isisubgr  47848  iscnrm3rlem3  48839