Theorem sselpwd 5288

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3446   ⊆ wss 3913  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567

This theorem is referenced by:  knatar  7307  marypha1  9379  fin1a2lem7  10351  canthp1lem2  10598  wunss  10657  ramub1lem1  16909  mreexd  17536  mreexexlemd  17538  mreexexlem4d  17541  opsrval  21484  selvfval  21564  cncls  22662  fbasrn  23272  rnelfmlem  23340  ustssel  23594  pwrssmgc  31930  crefi  32517  ldsysgenld  32848  ldgenpisyslem1  32851  bj-ismoored  35651  bj-imdirval2  35727  bj-iminvval2  35738  sticksstones2  40628  rfovcnvf1od  42398  fsovrfovd  42403  fsovfd  42406  fsovcnvlem  42407  ntrclsrcomplex  42429  clsk3nimkb  42434  clsk1indlem4  42438  clsk1indlem1  42439  ntrclsiso  42461  ntrclskb  42463  ntrclsk3  42464  ntrclsk13  42465  ntrneircomplex  42468  ntrneik3  42490  ntrneix3  42491  ntrneik13  42492  ntrneix13  42493  clsneircomplex  42497  clsneiel1  42502  neicvgrcomplex  42507  neicvgel1  42513  mnussd  42665  mnuprssd  42671  mnuop3d  42673  wessf1ornlem  43525  ovolsplit  44349  saliunclf  44683  iscnrm3rlem3  47095