Theorem sselpwd 5278

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911  𝒫 cpw 4559

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 5246

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 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561

This theorem is referenced by:  knatar  7314  marypha1  9361  fin1a2lem7  10335  canthp1lem2  10582  wunss  10641  ramub1lem1  16973  mreexd  17583  mreexexlemd  17585  mreexexlem4d  17588  opsrval  21986  selvfval  22054  cncls  23194  fbasrn  23804  rnelfmlem  23872  ustssel  24126  pwrssmgc  32972  exsslsb  33585  crefi  33830  ldsysgenld  34143  ldgenpisyslem1  34146  bj-ismoored  37088  bj-imdirval2  37164  bj-iminvval2  37175  sticksstones2  42128  rfovcnvf1od  43986  fsovrfovd  43991  fsovfd  43994  fsovcnvlem  43995  ntrclsrcomplex  44017  clsk3nimkb  44022  clsk1indlem4  44026  clsk1indlem1  44027  ntrclsiso  44049  ntrclskb  44051  ntrclsk3  44052  ntrclsk13  44053  ntrneircomplex  44056  ntrneik3  44078  ntrneix3  44079  ntrneik13  44080  ntrneix13  44081  clsneircomplex  44085  clsneiel1  44090  neicvgrcomplex  44095  neicvgel1  44101  mnussd  44245  mnuprssd  44251  mnuop3d  44253  wessf1ornlem  45172  dvnprodlem1  45937  ovolsplit  45979  saliunclf  46313  sge0f1o  46373  isisubgr  47855  iscnrm3rlem3  48923