Theorem sselpwd 5232

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3496   ⊆ wss 3938  𝒫 cpw 4541

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 2795  ax-sep 5205

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  knatar  7112  marypha1  8900  fin1a2lem7  9830  canthp1lem2  10077  wunss  10136  ramub1lem1  16364  mreexd  16915  mreexexlemd  16917  mreexexlem4d  16920  opsrval  20257  selvfval  20332  cncls  21884  fbasrn  22494  rnelfmlem  22562  ustssel  22816  crefi  31113  ldsysgenld  31421  ldgenpisyslem1  31424  bj-ismoored  34401  bj-imdirval2  34475  rfovcnvf1od  40357  fsovrfovd  40362  fsovfd  40365  fsovcnvlem  40366  ntrclsrcomplex  40392  clsk3nimkb  40397  clsk1indlem4  40401  clsk1indlem1  40402  ntrclsiso  40424  ntrclskb  40426  ntrclsk3  40427  ntrclsk13  40428  ntrneircomplex  40431  ntrneik3  40453  ntrneix3  40454  ntrneik13  40455  ntrneix13  40456  clsneircomplex  40460  clsneiel1  40465  neicvgrcomplex  40470  neicvgel1  40476  mnussd  40606  mnuprssd  40612  mnuop3d  40614  wessf1ornlem  41452  ovolsplit  42280