Theorem sselpwd 5289

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-pw 4558

This theorem is used by:  knatar  7367  marypha1  9426  fin1a2lem7  10484  canthp1lem2  10738  wunss  10797  ramub1lem1  17204  mreexd  17816  mreexexlemd  17818  mreexexlem4d  17821  opsrval  22355  selvfval  22428  cncls  23592  fbasrn  24203  rnelfmlem  24271  ustssel  24525  hashimaf1  33402  pwrssmgc  33561  esplyfv1  34201  exsslsb  34229  crefi  34479  ldsysgenld  34793  ldgenpisyslem1  34796  bj-ismoored  38028  bj-imdirval2  38105  bj-iminvval2  38116  sticksstones2  43198  rfovcnvf1od  45004  fsovrfovd  45009  fsovfd  45012  fsovcnvlem  45013  ntrclsrcomplex  45035  clsk3nimkb  45040  clsk1indlem4  45044  clsk1indlem1  45045  ntrclsiso  45067  ntrclskb  45069  ntrclsk3  45070  ntrclsk13  45071  ntrneircomplex  45074  ntrneik3  45096  ntrneix3  45097  ntrneik13  45098  ntrneix13  45099  clsneircomplex  45103  clsneiel1  45108  neicvgrcomplex  45113  neicvgel1  45119  mnussd  45247  mnuprssd  45253  mnuop3d  45255  wessf1ornlem  46200  dvnprodlem1  46956  ovolsplit  46998  saliunclf  47332  sge0f1o  47392  isisubgr  48960  iscnrm3rlem3  50050