| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sspwd | Structured version Visualization version GIF version | ||
| Description: The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
| Ref | Expression |
|---|---|
| sspwd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| Ref | Expression |
|---|---|
| sspwd | ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sspwd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
| 2 | sspw 4611 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ wss 3951 𝒫 cpw 4600 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: pweq 4614 pwel 5381 marypha1lem 9473 pwwf 9847 rankpwi 9863 ackbij2lem1 10258 fictb 10284 ssfin2 10360 ssfin3ds 10370 ttukeylem2 10550 hashbcss 17042 isacs1i 17700 mreacs 17701 acsfn 17702 isacs3lem 18587 isacs5lem 18590 tgcmp 23409 imastopn 23728 fgabs 23887 fgtr 23898 trfg 23899 ssufl 23926 alexsubb 24054 cfiluweak 24304 cmetss 25350 minveclem4a 25464 minveclem4 25466 madess 27915 ldsysgenld 34161 neibastop1 36360 neibastop2lem 36361 neibastop2 36362 sstotbnd2 37781 prjcrv0 42643 isnacs3 42721 aomclem2 43067 sge0iunmptlemre 46430 |
| Copyright terms: Public domain | W3C validator |