Theorem sselpwd 5299

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3461   ⊆ wss 3911  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-in 3918  df-ss 3928  df-pw 4567

This theorem is referenced by:  knatar  7356  marypha1  9394  fin1a2lem7  10390  canthp1lem2  10638  wunss  10697  ramub1lem1  17086  mreexd  17698  mreexexlemd  17700  mreexexlem4d  17703  opsrval  22166  selvfval  22239  cncls  23400  fbasrn  24010  rnelfmlem  24078  ustssel  24332  hashimaf1  33096  pwrssmgc  33261  esplyfv1  33904  exsslsb  33932  crefi  34182  ldsysgenld  34495  ldgenpisyslem1  34498  bj-ismoored  37672  bj-imdirval2  37750  bj-iminvval2  37761  sticksstones2  42839  rfovcnvf1od  44657  fsovrfovd  44662  fsovfd  44665  fsovcnvlem  44666  ntrclsrcomplex  44688  clsk3nimkb  44693  clsk1indlem4  44697  clsk1indlem1  44698  ntrclsiso  44720  ntrclskb  44722  ntrclsk3  44723  ntrclsk13  44724  ntrneircomplex  44727  ntrneik3  44749  ntrneix3  44750  ntrneik13  44751  ntrneix13  44752  clsneircomplex  44756  clsneiel1  44761  neicvgrcomplex  44766  neicvgel1  44772  mnussd  44900  mnuprssd  44906  mnuop3d  44908  wessf1ornlem  45830  dvnprodlem1  46587  ovolsplit  46629  saliunclf  46963  sge0f1o  47023  isisubgr  48551  iscnrm3rlem3  49640