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

Theorem sselpwd 5222
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 5220 . 2 (𝜑𝐴 ∈ V)
43, 2elpwd 4548 1 (𝜑𝐴 ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3495  wss 3935  𝒫 cpw 4537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-in 3942  df-ss 3951  df-pw 4539
This theorem is referenced by:  knatar  7099  marypha1  8887  fin1a2lem7  9817  canthp1lem2  10064  wunss  10123  ramub1lem1  16352  mreexd  16903  mreexexlemd  16905  mreexexlem4d  16908  opsrval  20185  selvfval  20260  cncls  21812  fbasrn  22422  rnelfmlem  22490  ustssel  22743  crefi  31011  ldsysgenld  31319  ldgenpisyslem1  31322  bj-ismoored  34294  bj-imdirval2  34366  rfovcnvf1od  40230  fsovrfovd  40235  fsovfd  40238  fsovcnvlem  40239  ntrclsrcomplex  40265  clsk3nimkb  40270  clsk1indlem4  40274  clsk1indlem1  40275  ntrclsiso  40297  ntrclskb  40299  ntrclsk3  40300  ntrclsk13  40301  ntrneircomplex  40304  ntrneik3  40326  ntrneix3  40327  ntrneik13  40328  ntrneix13  40329  clsneircomplex  40333  clsneiel1  40338  neicvgrcomplex  40343  neicvgel1  40349  mnussd  40479  mnuprssd  40485  mnuop3d  40487  wessf1ornlem  41325  ovolsplit  42154
  Copyright terms: Public domain W3C validator