Metamath Proof Explorer


Theorem sspwimp

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. For the biconditional, see sspwb . The proof sspwimp , using conventional notation, was translated from virtual deduction form, sspwimpVD , using a translation program. (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sspwimp AB𝒫A𝒫B

Proof

Step Hyp Ref Expression
1 vex xV
2 1 a1i xV
3 id ABAB
4 id x𝒫Ax𝒫A
5 elpwi x𝒫AxA
6 4 5 syl x𝒫AxA
7 sstr xAABxB
8 7 ancoms ABxAxB
9 3 6 8 syl2an ABx𝒫AxB
10 2 9 elpwgded ABx𝒫Ax𝒫B
11 2 9 10 uun0.1 ABx𝒫Ax𝒫B
12 11 ex ABx𝒫Ax𝒫B
13 12 alrimiv ABxx𝒫Ax𝒫B
14 dfss2 𝒫A𝒫Bxx𝒫Ax𝒫B
15 14 biimpri xx𝒫Ax𝒫B𝒫A𝒫B
16 13 15 syl AB𝒫A𝒫B
17 16 iin1 AB𝒫A𝒫B