Metamath Proof Explorer


Theorem sspwimpcf

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. sspwimpcf , using conventional notation, was translated from its virtual deduction form, sspwimpcfVD , using a translation program. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sspwimpcf A B 𝒫 A 𝒫 B

Proof

Step Hyp Ref Expression
1 vex x V
2 id A B A B
3 id x 𝒫 A x 𝒫 A
4 elpwi x 𝒫 A x A
5 3 4 syl x 𝒫 A x A
6 sstr2 x A A B x B
7 6 impcom A B x A x B
8 2 5 7 syl2an A B x 𝒫 A x B
9 elpwg x V x 𝒫 B x B
10 9 biimpar x V x B x 𝒫 B
11 1 8 10 eel021old A B x 𝒫 A x 𝒫 B
12 11 ex A B x 𝒫 A x 𝒫 B
13 12 alrimiv A B x x 𝒫 A x 𝒫 B
14 dfss2 𝒫 A 𝒫 B x x 𝒫 A x 𝒫 B
15 14 biimpri x x 𝒫 A x 𝒫 B 𝒫 A 𝒫 B
16 13 15 syl A B 𝒫 A 𝒫 B
17 16 iin1 A B 𝒫 A 𝒫 B