Theorem sselpwd 5298

Description: Membership in 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 5294	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
4	3, 2	elpwd 4567	1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904  𝒫 cpw 4561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921  df-pw 4563

This theorem is used by:  knatar  7357  marypha1  9392  fin1a2lem7  10396  canthp1lem2  10644  wunss  10703  ramub1lem1  17092  mreexd  17704  mreexexlemd  17706  mreexexlem4d  17709  opsrval  22208  selvfval  22281  cncls  23442  fbasrn  24052  rnelfmlem  24120  ustssel  24374  hashimaf1  33166  pwrssmgc  33329  esplyfv1  33968  exsslsb  33996  crefi  34246  ldsysgenld  34559  ldgenpisyslem1  34562  bj-ismoored  37777  bj-imdirval2  37855  bj-iminvval2  37866  sticksstones2  42942  rfovcnvf1od  44758  fsovrfovd  44763  fsovfd  44766  fsovcnvlem  44767  ntrclsrcomplex  44789  clsk3nimkb  44794  clsk1indlem4  44798  clsk1indlem1  44799  ntrclsiso  44821  ntrclskb  44823  ntrclsk3  44824  ntrclsk13  44825  ntrneircomplex  44828  ntrneik3  44850  ntrneix3  44851  ntrneik13  44852  ntrneix13  44853  clsneircomplex  44857  clsneiel1  44862  neicvgrcomplex  44867  neicvgel1  44873  mnussd  45001  mnuprssd  45007  mnuop3d  45009  wessf1ornlem  45931  dvnprodlem1  46688  ovolsplit  46730  saliunclf  47064  sge0f1o  47124  isisubgr  48655  iscnrm3rlem3  49748