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

Theorem sselpwd 4734
 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 4733 . . 3 (𝜑𝐴 ∈ V)
4 elpwg 4116 . . 3 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
53, 4syl 17 . 2 (𝜑 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
61, 5mpbird 246 1 (𝜑𝐴 ∈ 𝒫 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  𝒫 cpw 4108 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110 This theorem is referenced by:  fin1a2lem7  9111  ustssel  21819  ldsysgenld  29550  ldgenpisyslem1  29553  rfovcnvf1od  37318  fsovrfovd  37323  fsovfd  37326  fsovcnvlem  37327  ntrclsrcomplex  37353  clsk3nimkb  37358  clsk1indlem3  37361  clsk1indlem4  37362  clsk1indlem1  37363  ntrclsiso  37385  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrneircomplex  37392  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  clsneircomplex  37421  clsneiel1  37426  neicvgrcomplex  37431  neicvgel1  37437  ovolsplit  38881
 Copyright terms: Public domain W3C validator