MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sselpwd Structured version   Visualization version   GIF version

Theorem sselpwd 5197
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
StepHypRef Expression
1 sselpwd.1 . . 3 (𝜑𝐵𝑉)
2 sselpwd.2 . . 3 (𝜑𝐴𝐵)
31, 2ssexd 5195 . 2 (𝜑𝐴 ∈ V)
43, 2elpwd 4508 1 (𝜑𝐴 ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Vcvv 3444  wss 3884  𝒫 cpw 4500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-sep 5170
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-v 3446  df-in 3891  df-ss 3901  df-pw 4502
This theorem is referenced by:  knatar  7093  marypha1  8886  fin1a2lem7  9821  canthp1lem2  10068  wunss  10127  ramub1lem1  16355  mreexd  16908  mreexexlemd  16910  mreexexlem4d  16913  opsrval  20717  selvfval  20792  cncls  21882  fbasrn  22492  rnelfmlem  22560  ustssel  22814  pwrssmgc  30709  crefi  31200  ldsysgenld  31527  ldgenpisyslem1  31530  bj-ismoored  34517  bj-imdirval2  34593  bj-iminvval2  34604  rfovcnvf1od  40692  fsovrfovd  40697  fsovfd  40700  fsovcnvlem  40701  ntrclsrcomplex  40725  clsk3nimkb  40730  clsk1indlem4  40734  clsk1indlem1  40735  ntrclsiso  40757  ntrclskb  40759  ntrclsk3  40760  ntrclsk13  40761  ntrneircomplex  40764  ntrneik3  40786  ntrneix3  40787  ntrneik13  40788  ntrneix13  40789  clsneircomplex  40793  clsneiel1  40798  neicvgrcomplex  40803  neicvgel1  40809  mnussd  40958  mnuprssd  40964  mnuop3d  40966  wessf1ornlem  41798  ovolsplit  42617
  Copyright terms: Public domain W3C validator