Metamath Proof Explorer

Theorem sspwimpALT2

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 . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sspwimpALT2 A B 𝒫 A 𝒫 B


Step Hyp Ref Expression
1 vex x V
2 elpwi x 𝒫 A x A
3 id A B A B
4 2 3 sylan9ssr A B x 𝒫 A x B
5 elpwg x V x 𝒫 B x B
6 5 biimpar x V x B x 𝒫 B
7 1 4 6 sylancr A B x 𝒫 A x 𝒫 B
8 7 ex A B x 𝒫 A x 𝒫 B
9 8 ssrdv A B 𝒫 A 𝒫 B