Theorem sselpwd 5286

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917  𝒫 cpw 4566

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568

This theorem is referenced by:  knatar  7335  marypha1  9392  fin1a2lem7  10366  canthp1lem2  10613  wunss  10672  ramub1lem1  17004  mreexd  17610  mreexexlemd  17612  mreexexlem4d  17615  opsrval  21960  selvfval  22028  cncls  23168  fbasrn  23778  rnelfmlem  23846  ustssel  24100  pwrssmgc  32933  exsslsb  33599  crefi  33844  ldsysgenld  34157  ldgenpisyslem1  34160  bj-ismoored  37102  bj-imdirval2  37178  bj-iminvval2  37189  sticksstones2  42142  rfovcnvf1od  44000  fsovrfovd  44005  fsovfd  44008  fsovcnvlem  44009  ntrclsrcomplex  44031  clsk3nimkb  44036  clsk1indlem4  44040  clsk1indlem1  44041  ntrclsiso  44063  ntrclskb  44065  ntrclsk3  44066  ntrclsk13  44067  ntrneircomplex  44070  ntrneik3  44092  ntrneix3  44093  ntrneik13  44094  ntrneix13  44095  clsneircomplex  44099  clsneiel1  44104  neicvgrcomplex  44109  neicvgel1  44115  mnussd  44259  mnuprssd  44265  mnuop3d  44267  wessf1ornlem  45186  dvnprodlem1  45951  ovolsplit  45993  saliunclf  46327  sge0f1o  46387  isisubgr  47866  iscnrm3rlem3  48934