Theorem sselpwd 5298

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926  𝒫 cpw 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  knatar  7350  marypha1  9446  fin1a2lem7  10420  canthp1lem2  10667  wunss  10726  ramub1lem1  17046  mreexd  17654  mreexexlemd  17656  mreexexlem4d  17659  opsrval  22004  selvfval  22072  cncls  23212  fbasrn  23822  rnelfmlem  23890  ustssel  24144  pwrssmgc  32980  exsslsb  33636  crefi  33878  ldsysgenld  34191  ldgenpisyslem1  34194  bj-ismoored  37125  bj-imdirval2  37201  bj-iminvval2  37212  sticksstones2  42160  rfovcnvf1od  44028  fsovrfovd  44033  fsovfd  44036  fsovcnvlem  44037  ntrclsrcomplex  44059  clsk3nimkb  44064  clsk1indlem4  44068  clsk1indlem1  44069  ntrclsiso  44091  ntrclskb  44093  ntrclsk3  44094  ntrclsk13  44095  ntrneircomplex  44098  ntrneik3  44120  ntrneix3  44121  ntrneik13  44122  ntrneix13  44123  clsneircomplex  44127  clsneiel1  44132  neicvgrcomplex  44137  neicvgel1  44143  mnussd  44287  mnuprssd  44293  mnuop3d  44295  wessf1ornlem  45209  dvnprodlem1  45975  ovolsplit  46017  saliunclf  46351  sge0f1o  46411  isisubgr  47875  iscnrm3rlem3  48916