Theorem sselpwd 5283

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914  𝒫 cpw 4563

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  knatar  7332  marypha1  9385  fin1a2lem7  10359  canthp1lem2  10606  wunss  10665  ramub1lem1  16997  mreexd  17603  mreexexlemd  17605  mreexexlem4d  17608  opsrval  21953  selvfval  22021  cncls  23161  fbasrn  23771  rnelfmlem  23839  ustssel  24093  pwrssmgc  32926  exsslsb  33592  crefi  33837  ldsysgenld  34150  ldgenpisyslem1  34153  bj-ismoored  37095  bj-imdirval2  37171  bj-iminvval2  37182  sticksstones2  42135  rfovcnvf1od  43993  fsovrfovd  43998  fsovfd  44001  fsovcnvlem  44002  ntrclsrcomplex  44024  clsk3nimkb  44029  clsk1indlem4  44033  clsk1indlem1  44034  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrneircomplex  44063  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  clsneircomplex  44092  clsneiel1  44097  neicvgrcomplex  44102  neicvgel1  44108  mnussd  44252  mnuprssd  44258  mnuop3d  44260  wessf1ornlem  45179  dvnprodlem1  45944  ovolsplit  45986  saliunclf  46320  sge0f1o  46380  isisubgr  47862  iscnrm3rlem3  48930