Theorem iinrab2

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

	Ref	Expression
Assertion	iinrab2	|- ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph }

Proof

Step	Hyp	Ref	Expression
1		iineq1	|- ( A = (/) -> |^|_ x e. A { y e. B | ph } = |^|_ x e. (/) { y e. B | ph } )
2		0iin	|- |^|_ x e. (/) { y e. B | ph } = _V
3	1 2	eqtrdi	|- ( A = (/) -> |^|_ x e. A { y e. B | ph } = _V )
4	3	ineq1d	|- ( A = (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = ( _V i^i B ) )
5		incom	|- ( _V i^i B ) = ( B i^i _V )
6		inv1	|- ( B i^i _V ) = B
7	5 6	eqtri	|- ( _V i^i B ) = B
8	4 7	eqtrdi	|- ( A = (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = B )
9		rzal	|- ( A = (/) -> A. x e. A A. y e. B ph )
10		rabid2	|- ( B = { y e. B | A. x e. A ph } <-> A. y e. B A. x e. A ph )
11		ralcom	|- ( A. y e. B A. x e. A ph <-> A. x e. A A. y e. B ph )
12	10 11	bitr2i	|- ( A. x e. A A. y e. B ph <-> B = { y e. B | A. x e. A ph } )
13	9 12	sylib	|- ( A = (/) -> B = { y e. B | A. x e. A ph } )
14	8 13	eqtrd	|- ( A = (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph } )
15		iinrab	|- ( A =/= (/) -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )
16	15	ineq1d	|- ( A =/= (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = ( { y e. B | A. x e. A ph } i^i B ) )
17		ssrab2	|- { y e. B | A. x e. A ph } C_ B
18		dfss	|- ( { y e. B | A. x e. A ph } C_ B <-> { y e. B | A. x e. A ph } = ( { y e. B | A. x e. A ph } i^i B ) )
19	17 18	mpbi	|- { y e. B | A. x e. A ph } = ( { y e. B | A. x e. A ph } i^i B )
20	16 19	eqtr4di	|- ( A =/= (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph } )
21	14 20	pm2.61ine	|- ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph }