This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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