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	$$⊢𝒫\left(A\cap B\right)=𝒫A\cap 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		ssin	$$⊢\left(x\subseteq A\wedge x\subseteq B\right)\leftrightarrow x\subseteq A\cap B$$
2		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
3		velpw	$$⊢x\in 𝒫B\leftrightarrow x\subseteq B$$
4	2 3	anbi12i	$$⊢\left(x\in 𝒫A\wedge x\in 𝒫B\right)\leftrightarrow \left(x\subseteq A\wedge x\subseteq B\right)$$
5		velpw	$$⊢x\in 𝒫\left(A\cap B\right)\leftrightarrow x\subseteq A\cap B$$
6	1 4 5	3bitr4i	$$⊢\left(x\in 𝒫A\wedge x\in 𝒫B\right)\leftrightarrow x\in 𝒫\left(A\cap B\right)$$
7	6	ineqri	$$⊢𝒫A\cap 𝒫B=𝒫\left(A\cap B\right)$$
8	7	eqcomi	$$⊢𝒫\left(A\cap B\right)=𝒫A\cap 𝒫B$$