Metamath Proof Explorer

Theorem iinab

Description: Indexed intersection of a class abstraction. (Contributed by NM, 6-Dec-2011)

Ref Expression
Assertion iinab 
|- |^|_ x e. A { y | ph } = { y | A. x e. A ph }

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ y A
2 nfab1 
 |-  F/_ y { y | ph }
3 1 2 nfiin 
 |-  F/_ y |^|_ x e. A { y | ph }
4 nfab1 
 |-  F/_ y { y | A. x e. A ph }
5 3 4 cleqf 
 |-  ( |^|_ x e. A { y | ph } = { y | A. x e. A ph } <-> A. y ( y e. |^|_ x e. A { y | ph } <-> y e. { y | A. x e. A ph } ) )
6 abid 
 |-  ( y e. { y | ph } <-> ph )
7 6 ralbii 
 |-  ( A. x e. A y e. { y | ph } <-> A. x e. A ph )
8 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A { y | ph } <-> A. x e. A y e. { y | ph } ) )
9 8 elv 
 |-  ( y e. |^|_ x e. A { y | ph } <-> A. x e. A y e. { y | ph } )
10 abid 
 |-  ( y e. { y | A. x e. A ph } <-> A. x e. A ph )
11 7 9 10 3bitr4i 
 |-  ( y e. |^|_ x e. A { y | ph } <-> y e. { y | A. x e. A ph } )
12 5 11 mpgbir 
 |-  |^|_ x e. A { y | ph } = { y | A. x e. A ph }