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		abid	|- ( y e. { y | ph } <-> ph )
6	5	ralbii	|- ( A. x e. A y e. { y | ph } <-> A. x e. A ph )
7		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A { y | ph } <-> A. x e. A y e. { y | ph } ) )
8	7	elv	|- ( y e. |^|_ x e. A { y | ph } <-> A. x e. A y e. { y | ph } )
9		abid	|- ( y e. { y | A. x e. A ph } <-> A. x e. A ph )
10	6 8 9	3bitr4i	|- ( y e. |^|_ x e. A { y | ph } <-> y e. { y | A. x e. A ph } )
11	3 4 10	eqri	|- |^|_ x e. A { y | ph } = { y | A. x e. A ph }