![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sspwi | Structured version Visualization version GIF version |
Description: The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
Ref | Expression |
---|---|
sspwi.1 | ⊢ 𝐴 ⊆ 𝐵 |
Ref | Expression |
---|---|
sspwi | ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sspwi.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | sspw 4570 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | |
3 | 1, 2 | ax-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 |