Theorem sselpwd 5274

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902  𝒫 cpw 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-in 3909  df-ss 3919  df-pw 4557

This theorem is referenced by:  knatar  7305  marypha1  9341  fin1a2lem7  10320  canthp1lem2  10568  wunss  10627  ramub1lem1  16958  mreexd  17569  mreexexlemd  17571  mreexexlem4d  17574  opsrval  22005  selvfval  22081  cncls  23222  fbasrn  23832  rnelfmlem  23900  ustssel  24154  hashimaf1  32893  pwrssmgc  33084  esplyfv1  33729  exsslsb  33755  crefi  34006  ldsysgenld  34319  ldgenpisyslem1  34322  bj-ismoored  37314  bj-imdirval2  37390  bj-iminvval2  37401  sticksstones2  42469  rfovcnvf1od  44312  fsovrfovd  44317  fsovfd  44320  fsovcnvlem  44321  ntrclsrcomplex  44343  clsk3nimkb  44348  clsk1indlem4  44352  clsk1indlem1  44353  ntrclsiso  44375  ntrclskb  44377  ntrclsk3  44378  ntrclsk13  44379  ntrneircomplex  44382  ntrneik3  44404  ntrneix3  44405  ntrneik13  44406  ntrneix13  44407  clsneircomplex  44411  clsneiel1  44416  neicvgrcomplex  44421  neicvgel1  44427  mnussd  44571  mnuprssd  44577  mnuop3d  44579  wessf1ornlem  45496  dvnprodlem1  46257  ovolsplit  46299  saliunclf  46633  sge0f1o  46693  isisubgr  48175  iscnrm3rlem3  49254