Theorem sselpwd 5267

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903  𝒫 cpw 4551

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-in 3910  df-ss 3920  df-pw 4553

This theorem is referenced by:  knatar  7294  marypha1  9324  fin1a2lem7  10300  canthp1lem2  10547  wunss  10606  ramub1lem1  16938  mreexd  17548  mreexexlemd  17550  mreexexlem4d  17553  opsrval  21951  selvfval  22019  cncls  23159  fbasrn  23769  rnelfmlem  23837  ustssel  24091  pwrssmgc  32942  exsslsb  33563  crefi  33814  ldsysgenld  34127  ldgenpisyslem1  34130  bj-ismoored  37081  bj-imdirval2  37157  bj-iminvval2  37168  sticksstones2  42120  rfovcnvf1od  43977  fsovrfovd  43982  fsovfd  43985  fsovcnvlem  43986  ntrclsrcomplex  44008  clsk3nimkb  44013  clsk1indlem4  44017  clsk1indlem1  44018  ntrclsiso  44040  ntrclskb  44042  ntrclsk3  44043  ntrclsk13  44044  ntrneircomplex  44047  ntrneik3  44069  ntrneix3  44070  ntrneik13  44071  ntrneix13  44072  clsneircomplex  44076  clsneiel1  44081  neicvgrcomplex  44086  neicvgel1  44092  mnussd  44236  mnuprssd  44242  mnuop3d  44244  wessf1ornlem  45163  dvnprodlem1  45927  ovolsplit  45969  saliunclf  46303  sge0f1o  46363  isisubgr  47846  iscnrm3rlem3  48926