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

Theorem sspwi 4511
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 4510 . 2 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
31, 2ax-mp 5 1 𝒫 𝐴 ⊆ 𝒫 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3881  𝒫 cpw 4497
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499
This theorem is referenced by:  pwunss  4517  pwundif  4523  pwdom  8653  wdompwdom  9026  rankxplim  9292  hashbclem  13806  incexclem  15183  sscpwex  17077  wunfunc  17161  tsmsres  22749  cfilresi  23899  vitali  24217  sqff1o  25767  ldgenpisyslem1  31532  imambfm  31630  ballotlem2  31856  dssmapnvod  40719  gneispace  40835  sge0less  43029
  Copyright terms: Public domain W3C validator