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	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sspw	⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
2		ssel	⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 → ( { 𝑥 } ∈ 𝒫 𝐴 → { 𝑥 } ∈ 𝒫 𝐵 ) )
3		snex	⊢ { 𝑥 } ∈ V
4	3	elpw	⊢ ( { 𝑥 } ∈ 𝒫 𝐴 ↔ { 𝑥 } ⊆ 𝐴 )
5		vex	⊢ 𝑥 ∈ V
6	5	snss	⊢ ( 𝑥 ∈ 𝐴 ↔ { 𝑥 } ⊆ 𝐴 )
7	4 6	bitr4i	⊢ ( { 𝑥 } ∈ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴 )
8	3	elpw	⊢ ( { 𝑥 } ∈ 𝒫 𝐵 ↔ { 𝑥 } ⊆ 𝐵 )
9	5	snss	⊢ ( 𝑥 ∈ 𝐵 ↔ { 𝑥 } ⊆ 𝐵 )
10	8 9	bitr4i	⊢ ( { 𝑥 } ∈ 𝒫 𝐵 ↔ 𝑥 ∈ 𝐵 )
11	2 7 10	3imtr3g	⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
12	11	ssrdv	⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 → 𝐴 ⊆ 𝐵 )
13	1 12	impbii	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵 )