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 2145  Vcvv 3450   ⊆ wss 3898  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3905  df-ss 3915  df-pw 4558

This theorem is used by:  knatar  7355  marypha1  9404  fin1a2lem7  10455  canthp1lem2  10709  wunss  10768  ramub1lem1  17165  mreexd  17777  mreexexlemd  17779  mreexexlem4d  17782  opsrval  22316  selvfval  22389  cncls  23553  fbasrn  24164  rnelfmlem  24232  ustssel  24486  hashimaf1  33335  pwrssmgc  33494  esplyfv1  34134  exsslsb  34162  crefi  34412  ldsysgenld  34726  ldgenpisyslem1  34729  bj-ismoored  37948  bj-imdirval2  38024  bj-iminvval2  38035  sticksstones2  43117  rfovcnvf1od  44948  fsovrfovd  44953  fsovfd  44956  fsovcnvlem  44957  ntrclsrcomplex  44979  clsk3nimkb  44984  clsk1indlem4  44988  clsk1indlem1  44989  ntrclsiso  45011  ntrclskb  45013  ntrclsk3  45014  ntrclsk13  45015  ntrneircomplex  45018  ntrneik3  45040  ntrneix3  45041  ntrneik13  45042  ntrneix13  45043  clsneircomplex  45047  clsneiel1  45052  neicvgrcomplex  45057  neicvgel1  45063  mnussd  45191  mnuprssd  45197  mnuop3d  45199  wessf1ornlem  46121  dvnprodlem1  46878  ovolsplit  46920  saliunclf  47254  sge0f1o  47314  isisubgr  48882  iscnrm3rlem3  49972