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

Theorem sselpwd 5283
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 5281 . 2 (𝜑𝐴 ∈ V)
43, 2elpwd 4566 1 (𝜑𝐴 ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  Vcvv 3445  wss 3910  𝒫 cpw 4560
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-in 3917  df-ss 3927  df-pw 4562
This theorem is referenced by:  knatar  7301  marypha1  9369  fin1a2lem7  10341  canthp1lem2  10588  wunss  10647  ramub1lem1  16897  mreexd  17521  mreexexlemd  17523  mreexexlem4d  17526  opsrval  21445  selvfval  21525  cncls  22623  fbasrn  23233  rnelfmlem  23301  ustssel  23555  pwrssmgc  31804  crefi  32368  ldsysgenld  32699  ldgenpisyslem1  32702  bj-ismoored  35568  bj-imdirval2  35644  bj-iminvval2  35655  sticksstones2  40545  rfovcnvf1od  42257  fsovrfovd  42262  fsovfd  42265  fsovcnvlem  42266  ntrclsrcomplex  42288  clsk3nimkb  42293  clsk1indlem4  42297  clsk1indlem1  42298  ntrclsiso  42320  ntrclskb  42322  ntrclsk3  42323  ntrclsk13  42324  ntrneircomplex  42327  ntrneik3  42349  ntrneix3  42350  ntrneik13  42351  ntrneix13  42352  clsneircomplex  42356  clsneiel1  42361  neicvgrcomplex  42366  neicvgel1  42372  mnussd  42524  mnuprssd  42530  mnuop3d  42532  wessf1ornlem  43378  ovolsplit  44200  saliunclf  44534  iscnrm3rlem3  46946
  Copyright terms: Public domain W3C validator