Theorem sselpwd 5274

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

Syntax hints:   → wi 4   ∈ wcel 2132  Vcvv 3444   ⊆ wss 3895  𝒫 cpw 4545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1097  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-in 3902  df-ss 3912  df-pw 4547

This theorem is referenced by:  knatar  7326  marypha1  9366  fin1a2lem7  10349  canthp1lem2  10597  wunss  10656  ramub1lem1  17034  mreexd  17646  mreexexlemd  17648  mreexexlem4d  17651  opsrval  22068  selvfval  22141  cncls  23303  fbasrn  23913  rnelfmlem  23981  ustssel  24235  hashimaf1  32952  pwrssmgc  33128  esplyfv1  33810  exsslsb  33838  crefi  34088  ldsysgenld  34401  ldgenpisyslem1  34404  bj-ismoored  37535  bj-imdirval2  37613  bj-iminvval2  37624  sticksstones2  42702  rfovcnvf1od  44518  fsovrfovd  44523  fsovfd  44526  fsovcnvlem  44527  ntrclsrcomplex  44549  clsk3nimkb  44554  clsk1indlem4  44558  clsk1indlem1  44559  ntrclsiso  44581  ntrclskb  44583  ntrclsk3  44584  ntrclsk13  44585  ntrneircomplex  44588  ntrneik3  44610  ntrneix3  44611  ntrneik13  44612  ntrneix13  44613  clsneircomplex  44617  clsneiel1  44622  neicvgrcomplex  44627  neicvgel1  44633  mnussd  44777  mnuprssd  44783  mnuop3d  44785  wessf1ornlem  45701  dvnprodlem1  46458  ovolsplit  46500  saliunclf  46834  sge0f1o  46894  isisubgr  48422  iscnrm3rlem3  49501