Theorem sselpwd 5277

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  knatar  7315  marypha1  9351  fin1a2lem7  10330  canthp1lem2  10578  wunss  10637  ramub1lem1  16968  mreexd  17579  mreexexlemd  17581  mreexexlem4d  17584  opsrval  22018  selvfval  22094  cncls  23235  fbasrn  23845  rnelfmlem  23913  ustssel  24167  hashimaf1  32908  pwrssmgc  33099  esplyfv1  33752  exsslsb  33780  crefi  34031  ldsysgenld  34344  ldgenpisyslem1  34347  bj-ismoored  37387  bj-imdirval2  37465  bj-iminvval2  37476  sticksstones2  42546  rfovcnvf1od  44389  fsovrfovd  44394  fsovfd  44397  fsovcnvlem  44398  ntrclsrcomplex  44420  clsk3nimkb  44425  clsk1indlem4  44429  clsk1indlem1  44430  ntrclsiso  44452  ntrclskb  44454  ntrclsk3  44455  ntrclsk13  44456  ntrneircomplex  44459  ntrneik3  44481  ntrneix3  44482  ntrneik13  44483  ntrneix13  44484  clsneircomplex  44488  clsneiel1  44493  neicvgrcomplex  44498  neicvgel1  44504  mnussd  44648  mnuprssd  44654  mnuop3d  44656  wessf1ornlem  45573  dvnprodlem1  46333  ovolsplit  46375  saliunclf  46709  sge0f1o  46769  isisubgr  48251  iscnrm3rlem3  49330