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

Theorem sselpwd 4915
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 4913 . . 3 (𝜑𝐴 ∈ V)
4 elpwg 4274 . . 3 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
53, 4syl 17 . 2 (𝜑 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
61, 5mpbird 247 1 (𝜑𝐴 ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2103  Vcvv 3304  wss 3680  𝒫 cpw 4266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-in 3687  df-ss 3694  df-pw 4268
This theorem is referenced by:  knatar  6722  fin1a2lem7  9341  wunss  9647  mreexd  16425  mreexexlemd  16427  ustssel  22131  crefi  30144  ldsysgenld  30453  ldgenpisyslem1  30456  rfovcnvf1od  38717  fsovrfovd  38722  fsovfd  38725  fsovcnvlem  38726  ntrclsrcomplex  38752  clsk3nimkb  38757  clsk1indlem3  38760  clsk1indlem4  38761  clsk1indlem1  38762  ntrclsiso  38784  ntrclskb  38786  ntrclsk3  38787  ntrclsk13  38788  ntrneircomplex  38791  ntrneik3  38813  ntrneix3  38814  ntrneik13  38815  ntrneix13  38816  clsneircomplex  38820  clsneiel1  38825  neicvgrcomplex  38830  neicvgel1  38836  ovolsplit  40625
  Copyright terms: Public domain W3C validator