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  9128  wdompwdom  9572  rankxplim  9873  hashbclem  14410  incexclem  15781  sscpwex  17761  wunfunc  17848  wunfuncOLD  17849  tsmsres  23647  cfilresi  24811  vitali  25129  sqff1o  26683  ldgenpisyslem1  33156  imambfm  33256  ballotlem2  33482  dssmapnvod  42761  gneispace  42875  sge0less  45098
  Copyright terms: Public domain W3C validator