Theorem sselpwd 5286

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

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456   ⊆ wss 3906  𝒫 cpw 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923  df-pw 4559

This theorem is referenced by:  knatar  7343  marypha1  9382  fin1a2lem7  10365  canthp1lem2  10613  wunss  10672  ramub1lem1  17064  mreexd  17676  mreexexlemd  17678  mreexexlem4d  17681  opsrval  22101  selvfval  22174  cncls  23336  fbasrn  23946  rnelfmlem  24014  ustssel  24268  hashimaf1  33015  pwrssmgc  33180  esplyfv1  33868  exsslsb  33896  crefi  34146  ldsysgenld  34459  ldgenpisyslem1  34462  bj-ismoored  37602  bj-imdirval2  37680  bj-iminvval2  37691  sticksstones2  42769  rfovcnvf1od  44585  fsovrfovd  44590  fsovfd  44593  fsovcnvlem  44594  ntrclsrcomplex  44616  clsk3nimkb  44621  clsk1indlem4  44625  clsk1indlem1  44626  ntrclsiso  44648  ntrclskb  44650  ntrclsk3  44651  ntrclsk13  44652  ntrneircomplex  44655  ntrneik3  44677  ntrneix3  44678  ntrneik13  44679  ntrneix13  44680  clsneircomplex  44684  clsneiel1  44689  neicvgrcomplex  44694  neicvgel1  44700  mnussd  44844  mnuprssd  44850  mnuop3d  44852  wessf1ornlem  45768  dvnprodlem1  46525  ovolsplit  46567  saliunclf  46901  sge0f1o  46961  isisubgr  48489  iscnrm3rlem3  49568