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 4512 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3853 𝒫 cpw 4499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-in 3860 df-ss 3870 df-pw 4501 |
This theorem is referenced by: pwunss 4519 pwundif 4525 pwdom 8776 wdompwdom 9172 rankxplim 9460 hashbclem 13981 incexclem 15363 sscpwex 17274 wunfunc 17359 wunfuncOLD 17360 tsmsres 22995 cfilresi 24146 vitali 24464 sqff1o 26018 ldgenpisyslem1 31797 imambfm 31895 ballotlem2 32121 dssmapnvod 41246 gneispace 41362 sge0less 43548 |
Copyright terms: Public domain | W3C validator |