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  32943  exsslsb  33569  crefi  33820  ldsysgenld  34133  ldgenpisyslem1  34136  bj-ismoored  37091  bj-imdirval2  37167  bj-iminvval2  37178  sticksstones2  42130  rfovcnvf1od  43987  fsovrfovd  43992  fsovfd  43995  fsovcnvlem  43996  ntrclsrcomplex  44018  clsk3nimkb  44023  clsk1indlem4  44027  clsk1indlem1  44028  ntrclsiso  44050  ntrclskb  44052  ntrclsk3  44053  ntrclsk13  44054  ntrneircomplex  44057  ntrneik3  44079  ntrneix3  44080  ntrneik13  44081  ntrneix13  44082  clsneircomplex  44086  clsneiel1  44091  neicvgrcomplex  44096  neicvgel1  44102  mnussd  44246  mnuprssd  44252  mnuop3d  44254  wessf1ornlem  45173  dvnprodlem1  45937  ovolsplit  45979  saliunclf  46313  sge0f1o  46373  isisubgr  47856  iscnrm3rlem3  48936