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

Theorem sspwi 4614
Description: The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.)
Hypothesis
Ref Expression
sspwi.1 𝐴𝐵
Assertion
Ref Expression
sspwi 𝒫 𝐴 ⊆ 𝒫 𝐵

Proof of Theorem sspwi
StepHypRef Expression
1 sspwi.1 . 2 𝐴𝐵
2 sspw 4613 . 2 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
31, 2ax-mp 5 1 𝒫 𝐴 ⊆ 𝒫 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3948  𝒫 cpw 4602
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 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604
This theorem is referenced by:  pwunss  4620  pwundif  4626  pwdom  9131  wdompwdom  9575  rankxplim  9876  hashbclem  14415  incexclem  15786  sscpwex  17766  wunfunc  17853  wunfuncOLD  17854  tsmsres  23868  cfilresi  25036  vitali  25354  sqff1o  26910  ldgenpisyslem1  33447  imambfm  33547  ballotlem2  33773  dssmapnvod  43073  gneispace  43187  sge0less  45407
  Copyright terms: Public domain W3C validator