Theorem iinpw

Description: The power class of an intersection in terms of indexed intersection. Exercise 24(a) of Enderton p. 33. (Contributed by NM, 29-Nov-2003)

	Ref	Expression
Assertion	iinpw	|- ~P |^| A = |^|_ x e. A ~P x

Proof

Step	Hyp	Ref	Expression
1		ssint	|- ( y C_ |^| A <-> A. x e. A y C_ x )
2		velpw	|- ( y e. ~P x <-> y C_ x )
3	2	ralbii	|- ( A. x e. A y e. ~P x <-> A. x e. A y C_ x )
4	1 3	bitr4i	|- ( y C_ |^| A <-> A. x e. A y e. ~P x )
5		velpw	|- ( y e. ~P |^| A <-> y C_ |^| A )
6		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A ~P x <-> A. x e. A y e. ~P x ) )
7	6	elv	|- ( y e. |^|_ x e. A ~P x <-> A. x e. A y e. ~P x )
8	4 5 7	3bitr4i	|- ( y e. ~P |^| A <-> y e. |^|_ x e. A ~P x )
9	8	eqriv	|- ~P |^| A = |^|_ x e. A ~P x