# 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 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}\subseteq {B}\to 𝒫{A}\subseteq 𝒫{B}$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{x}\in \mathrm{V}$
2 elpwi ${⊢}{x}\in 𝒫{A}\to {x}\subseteq {A}$
3 id ${⊢}{A}\subseteq {B}\to {A}\subseteq {B}$
4 2 3 sylan9ssr ${⊢}\left({A}\subseteq {B}\wedge {x}\in 𝒫{A}\right)\to {x}\subseteq {B}$
5 elpwg ${⊢}{x}\in \mathrm{V}\to \left({x}\in 𝒫{B}↔{x}\subseteq {B}\right)$
6 5 biimpar ${⊢}\left({x}\in \mathrm{V}\wedge {x}\subseteq {B}\right)\to {x}\in 𝒫{B}$
7 1 4 6 sylancr ${⊢}\left({A}\subseteq {B}\wedge {x}\in 𝒫{A}\right)\to {x}\in 𝒫{B}$
8 7 ex ${⊢}{A}\subseteq {B}\to \left({x}\in 𝒫{A}\to {x}\in 𝒫{B}\right)$
9 8 ssrdv ${⊢}{A}\subseteq {B}\to 𝒫{A}\subseteq 𝒫{B}$