Theorem sselpwd 5259

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3885  𝒫 cpw 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3892  df-ss 3902  df-pw 4534

This theorem is referenced by:  knatar  7305  marypha1  9341  fin1a2lem7  10323  canthp1lem2  10571  wunss  10630  ramub1lem1  16992  mreexd  17603  mreexexlemd  17605  mreexexlem4d  17608  opsrval  22026  selvfval  22099  cncls  23261  fbasrn  23871  rnelfmlem  23939  ustssel  24193  hashimaf1  32907  pwrssmgc  33083  esplyfv1  33765  exsslsb  33793  crefi  34043  ldsysgenld  34356  ldgenpisyslem1  34359  bj-ismoored  37480  bj-imdirval2  37558  bj-iminvval2  37569  sticksstones2  42647  rfovcnvf1od  44463  fsovrfovd  44468  fsovfd  44471  fsovcnvlem  44472  ntrclsrcomplex  44494  clsk3nimkb  44499  clsk1indlem4  44503  clsk1indlem1  44504  ntrclsiso  44526  ntrclskb  44528  ntrclsk3  44529  ntrclsk13  44530  ntrneircomplex  44533  ntrneik3  44555  ntrneix3  44556  ntrneik13  44557  ntrneix13  44558  clsneircomplex  44562  clsneiel1  44567  neicvgrcomplex  44572  neicvgel1  44578  mnussd  44722  mnuprssd  44728  mnuop3d  44730  wessf1ornlem  45646  dvnprodlem1  46403  ovolsplit  46445  saliunclf  46779  sge0f1o  46839  isisubgr  48367  iscnrm3rlem3  49446