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 4538 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3924 𝒫 cpw 4525 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3488 df-in 3931 df-ss 3940 df-pw 4527 |
This theorem is referenced by: pwunss 4545 pwundif 4551 pwdom 8655 wdompwdom 9028 rankxplim 9294 hashbclem 13800 incexclem 15176 sscpwex 17068 wunfunc 17152 tsmsres 22735 cfilresi 23881 vitali 24197 sqff1o 25745 ldgenpisyslem1 31429 imambfm 31527 ballotlem2 31753 dssmapnvod 40439 gneispace 40557 sge0less 42747 |
Copyright terms: Public domain | W3C validator |