Theorem sselpwd 5230

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494   ⊆ wss 3936  𝒫 cpw 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  knatar  7110  marypha1  8898  fin1a2lem7  9828  canthp1lem2  10075  wunss  10134  ramub1lem1  16362  mreexd  16913  mreexexlemd  16915  mreexexlem4d  16918  opsrval  20255  selvfval  20330  cncls  21882  fbasrn  22492  rnelfmlem  22560  ustssel  22814  crefi  31111  ldsysgenld  31419  ldgenpisyslem1  31422  bj-ismoored  34402  bj-imdirval2  34476  rfovcnvf1od  40399  fsovrfovd  40404  fsovfd  40407  fsovcnvlem  40408  ntrclsrcomplex  40434  clsk3nimkb  40439  clsk1indlem4  40443  clsk1indlem1  40444  ntrclsiso  40466  ntrclskb  40468  ntrclsk3  40469  ntrclsk13  40470  ntrneircomplex  40473  ntrneik3  40495  ntrneix3  40496  ntrneik13  40497  ntrneix13  40498  clsneircomplex  40502  clsneiel1  40507  neicvgrcomplex  40512  neicvgel1  40518  mnussd  40648  mnuprssd  40654  mnuop3d  40656  wessf1ornlem  41494  ovolsplit  42322