Description: If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of TakeutiZaring p. 18. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sspwimpALT2 | |- ( A C_ B -> ~P A C_ ~P B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | elpwi | |- ( x e. ~P A -> x C_ A ) |
|
| 3 | id | |- ( A C_ B -> A C_ B ) |
|
| 4 | 2 3 | sylan9ssr | |- ( ( A C_ B /\ x e. ~P A ) -> x C_ B ) |
| 5 | elpwg | |- ( x e. _V -> ( x e. ~P B <-> x C_ B ) ) |
|
| 6 | 5 | biimpar | |- ( ( x e. _V /\ x C_ B ) -> x e. ~P B ) |
| 7 | 1 4 6 | sylancr | |- ( ( A C_ B /\ x e. ~P A ) -> x e. ~P B ) |
| 8 | 7 | ex | |- ( A C_ B -> ( x e. ~P A -> x e. ~P B ) ) |
| 9 | 8 | ssrdv | |- ( A C_ B -> ~P A C_ ~P B ) |