Theorem sselpwd 5269

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889  𝒫 cpw 4541

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 2708  ax-sep 5231

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906  df-pw 4543

This theorem is referenced by:  knatar  7312  marypha1  9347  fin1a2lem7  10328  canthp1lem2  10576  wunss  10635  ramub1lem1  16997  mreexd  17608  mreexexlemd  17610  mreexexlem4d  17613  opsrval  22024  selvfval  22100  cncls  23239  fbasrn  23849  rnelfmlem  23917  ustssel  24171  hashimaf1  32884  pwrssmgc  33060  esplyfv1  33713  exsslsb  33741  crefi  33991  ldsysgenld  34304  ldgenpisyslem1  34307  bj-ismoored  37419  bj-imdirval2  37497  bj-iminvval2  37508  sticksstones2  42586  rfovcnvf1od  44431  fsovrfovd  44436  fsovfd  44439  fsovcnvlem  44440  ntrclsrcomplex  44462  clsk3nimkb  44467  clsk1indlem4  44471  clsk1indlem1  44472  ntrclsiso  44494  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ntrneircomplex  44501  ntrneik3  44523  ntrneix3  44524  ntrneik13  44525  ntrneix13  44526  clsneircomplex  44530  clsneiel1  44535  neicvgrcomplex  44540  neicvgel1  44546  mnussd  44690  mnuprssd  44696  mnuop3d  44698  wessf1ornlem  45615  dvnprodlem1  46374  ovolsplit  46416  saliunclf  46750  sge0f1o  46810  isisubgr  48338  iscnrm3rlem3  49417