Theorem sselpwd 5346

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  knatar  7393  marypha1  9503  fin1a2lem7  10475  canthp1lem2  10722  wunss  10781  ramub1lem1  17073  mreexd  17700  mreexexlemd  17702  mreexexlem4d  17705  opsrval  22087  selvfval  22161  cncls  23303  fbasrn  23913  rnelfmlem  23981  ustssel  24235  pwrssmgc  32973  crefi  33793  ldsysgenld  34124  ldgenpisyslem1  34127  bj-ismoored  37073  bj-imdirval2  37149  bj-iminvval2  37160  sticksstones2  42104  rfovcnvf1od  43966  fsovrfovd  43971  fsovfd  43974  fsovcnvlem  43975  ntrclsrcomplex  43997  clsk3nimkb  44002  clsk1indlem4  44006  clsk1indlem1  44007  ntrclsiso  44029  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  ntrneircomplex  44036  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  clsneircomplex  44065  clsneiel1  44070  neicvgrcomplex  44075  neicvgel1  44081  mnussd  44232  mnuprssd  44238  mnuop3d  44240  wessf1ornlem  45092  ovolsplit  45909  saliunclf  46243  isisubgr  47734  iscnrm3rlem3  48622