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

Theorem sspwi 4571
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 4570 . 2 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
31, 2ax-mp 5 1 𝒫 𝐴 ⊆ 𝒫 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3909  𝒫 cpw 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926  df-pw 4561
This theorem is referenced by:  pwunss  4577  pwundif  4583  pwdom  9032  wdompwdom  9473  rankxplim  9774  hashbclem  14303  incexclem  15681  sscpwex  17658  wunfunc  17745  wunfuncOLD  17746  tsmsres  23447  cfilresi  24611  vitali  24929  sqff1o  26483  ldgenpisyslem1  32566  imambfm  32666  ballotlem2  32892  dssmapnvod  42197  gneispace  42311  sge0less  44528
  Copyright terms: Public domain W3C validator