Description: The powerclass preserves inclusion. See sspwb for the biconditional version. (Contributed by NM, 13-Oct-1996) Extract forward implication of sspwb since it requires fewer axioms. (Revised by BJ, 13-Apr-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sspw | |- ( A C_ B -> ~P A C_ ~P B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sstr2 | |- ( x C_ A -> ( A C_ B -> x C_ B ) ) |
|
| 2 | 1 | com12 | |- ( A C_ B -> ( x C_ A -> x C_ B ) ) |
| 3 | velpw | |- ( x e. ~P A <-> x C_ A ) |
|
| 4 | velpw | |- ( x e. ~P B <-> x C_ B ) |
|
| 5 | 2 3 4 | 3imtr4g | |- ( A C_ B -> ( x e. ~P A -> x e. ~P B ) ) |
| 6 | 5 | ssrdv | |- ( A C_ B -> ~P A C_ ~P B ) |