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	|- ~P ( A i^i B ) = ( ~P A i^i ~P B )

Proof

Step	Hyp	Ref	Expression
1		ssin	|- ( ( x C_ A /\ x C_ B ) <-> x C_ ( A i^i B ) )
2		velpw	|- ( x e. ~P A <-> x C_ A )
3		velpw	|- ( x e. ~P B <-> x C_ B )
4	2 3	anbi12i	|- ( ( x e. ~P A /\ x e. ~P B ) <-> ( x C_ A /\ x C_ B ) )
5		velpw	|- ( x e. ~P ( A i^i B ) <-> x C_ ( A i^i B ) )
6	1 4 5	3bitr4i	|- ( ( x e. ~P A /\ x e. ~P B ) <-> x e. ~P ( A i^i B ) )
7	6	ineqri	|- ( ~P A i^i ~P B ) = ~P ( A i^i B )
8	7	eqcomi	|- ~P ( A i^i B ) = ( ~P A i^i ~P B )