Theorem pwin

Description: The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of Mendelson p. 235. (Contributed by NM, 23-Nov-2003)

	Ref	Expression
Assertion	pwin	⊢ 𝒫 ( 𝐴 ∩ 𝐵 ) = ( 𝒫 𝐴 ∩ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssin	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
2		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
3		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 )
4	2 3	anbi12i	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ∈ 𝒫 𝐵 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) )
5		velpw	⊢ ( 𝑥 ∈ 𝒫 ( 𝐴 ∩ 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
6	1 4 5	3bitr4i	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ∈ 𝒫 𝐵 ) ↔ 𝑥 ∈ 𝒫 ( 𝐴 ∩ 𝐵 ) )
7	6	ineqri	⊢ ( 𝒫 𝐴 ∩ 𝒫 𝐵 ) = 𝒫 ( 𝐴 ∩ 𝐵 )
8	7	eqcomi	⊢ 𝒫 ( 𝐴 ∩ 𝐵 ) = ( 𝒫 𝐴 ∩ 𝒫 𝐵 )