Theorem sselpwd 5333

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

Syntax hints:   → wi 4   ∈ wcel 2099  Vcvv 3462   ⊆ wss 3947  𝒫 cpw 4607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-in 3954  df-ss 3964  df-pw 4609

This theorem is referenced by:  knatar  7369  marypha1  9477  fin1a2lem7  10449  canthp1lem2  10696  wunss  10755  ramub1lem1  17028  mreexd  17655  mreexexlemd  17657  mreexexlem4d  17660  opsrval  22053  selvfval  22129  cncls  23269  fbasrn  23879  rnelfmlem  23947  ustssel  24201  pwrssmgc  32870  crefi  33662  ldsysgenld  33993  ldgenpisyslem1  33996  bj-ismoored  36814  bj-imdirval2  36890  bj-iminvval2  36901  sticksstones2  41845  rfovcnvf1od  43671  fsovrfovd  43676  fsovfd  43679  fsovcnvlem  43680  ntrclsrcomplex  43702  clsk3nimkb  43707  clsk1indlem4  43711  clsk1indlem1  43712  ntrclsiso  43734  ntrclskb  43736  ntrclsk3  43737  ntrclsk13  43738  ntrneircomplex  43741  ntrneik3  43763  ntrneix3  43764  ntrneik13  43765  ntrneix13  43766  clsneircomplex  43770  clsneiel1  43775  neicvgrcomplex  43780  neicvgel1  43786  mnussd  43937  mnuprssd  43943  mnuop3d  43945  wessf1ornlem  44792  ovolsplit  45609  saliunclf  45943  isisubgr  47429  iscnrm3rlem3  48276