Theorem sspwb

Description: The powerclass construction preserves and reflects inclusion. Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of TakeutiZaring p. 18. (Contributed by NM, 13-Oct-1996)

	Ref	Expression
Assertion	sspwb	$$⊢A\subseteq B\leftrightarrow 𝒫A\subseteq 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		sspw	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$
2		ssel	$$⊢𝒫A\subseteq 𝒫B\to \left(\left\{x\right\}\in 𝒫A\to \left\{x\right\}\in 𝒫B\right)$$
3		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
4	3	elpw	$$⊢\left\{x\right\}\in 𝒫A\leftrightarrow \left\{x\right\}\subseteq A$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	snss	$$⊢x\in A\leftrightarrow \left\{x\right\}\subseteq A$$
7	4 6	bitr4i	$$⊢\left\{x\right\}\in 𝒫A\leftrightarrow x\in A$$
8	3	elpw	$$⊢\left\{x\right\}\in 𝒫B\leftrightarrow \left\{x\right\}\subseteq B$$
9	5	snss	$$⊢x\in B\leftrightarrow \left\{x\right\}\subseteq B$$
10	8 9	bitr4i	$$⊢\left\{x\right\}\in 𝒫B\leftrightarrow x\in B$$
11	2 7 10	3imtr3g	$$⊢𝒫A\subseteq 𝒫B\to \left(x\in A\to x\in B\right)$$
12	11	ssrdv	$$⊢𝒫A\subseteq 𝒫B\to A\subseteq B$$
13	1 12	impbii	$$⊢A\subseteq B\leftrightarrow 𝒫A\subseteq 𝒫B$$