Theorem sselpwd 5297

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902  𝒫 cpw 4560

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 2734  ax-sep 5255

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-pw 4562

This theorem is used by:  knatar  7363  marypha1  9407  fin1a2lem7  10411  canthp1lem2  10665  wunss  10724  ramub1lem1  17122  mreexd  17734  mreexexlemd  17736  mreexexlem4d  17739  opsrval  22263  selvfval  22336  cncls  23500  fbasrn  24111  rnelfmlem  24179  ustssel  24433  hashimaf1  33268  pwrssmgc  33427  esplyfv1  34066  exsslsb  34094  crefi  34344  ldsysgenld  34658  ldgenpisyslem1  34661  bj-ismoored  37844  bj-imdirval2  37922  bj-iminvval2  37933  sticksstones2  43000  rfovcnvf1od  44831  fsovrfovd  44836  fsovfd  44839  fsovcnvlem  44840  ntrclsrcomplex  44862  clsk3nimkb  44867  clsk1indlem4  44871  clsk1indlem1  44872  ntrclsiso  44894  ntrclskb  44896  ntrclsk3  44897  ntrclsk13  44898  ntrneircomplex  44901  ntrneik3  44923  ntrneix3  44924  ntrneik13  44925  ntrneix13  44926  clsneircomplex  44930  clsneiel1  44935  neicvgrcomplex  44940  neicvgel1  44946  mnussd  45074  mnuprssd  45080  mnuop3d  45082  wessf1ornlem  46004  dvnprodlem1  46761  ovolsplit  46803  saliunclf  47137  sge0f1o  47197  isisubgr  48765  iscnrm3rlem3  49855