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

Theorem sselpwd 4805
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.2 . 2 (𝜑𝐴𝐵)
2 sselpwd.1 . . . 4 (𝜑𝐵𝑉)
32, 1ssexd 4803 . . 3 (𝜑𝐴 ∈ V)
4 elpwg 4164 . . 3 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
53, 4syl 17 . 2 (𝜑 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
61, 5mpbird 247 1 (𝜑𝐴 ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 1989  Vcvv 3198  wss 3572  𝒫 cpw 4156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-in 3579  df-ss 3586  df-pw 4158
This theorem is referenced by:  knatar  6604  fin1a2lem7  9225  wunss  9531  mreexd  16296  mreexexlemd  16298  ustssel  22003  crefi  29899  ldsysgenld  30208  ldgenpisyslem1  30211  rfovcnvf1od  38124  fsovrfovd  38129  fsovfd  38132  fsovcnvlem  38133  ntrclsrcomplex  38159  clsk3nimkb  38164  clsk1indlem3  38167  clsk1indlem4  38168  clsk1indlem1  38169  ntrclsiso  38191  ntrclskb  38193  ntrclsk3  38194  ntrclsk13  38195  ntrneircomplex  38198  ntrneik3  38220  ntrneix3  38221  ntrneik13  38222  ntrneix13  38223  clsneircomplex  38227  clsneiel1  38232  neicvgrcomplex  38237  neicvgel1  38243  ovolsplit  39974
  Copyright terms: Public domain W3C validator