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		inv1	|- ( B i^i _V ) = B
6	5	ineqcomi	|- ( _V i^i B ) = B
7	4 6	eqtrdi	|- ( A = (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = B )
8		rzal	|- ( A = (/) -> A. x e. A A. y e. B ph )
9		rabid2	|- ( B = { y e. B | A. x e. A ph } <-> A. y e. B A. x e. A ph )
10		ralcom	|- ( A. y e. B A. x e. A ph <-> A. x e. A A. y e. B ph )
11	9 10	bitr2i	|- ( A. x e. A A. y e. B ph <-> B = { y e. B | A. x e. A ph } )
12	8 11	sylib	|- ( A = (/) -> B = { y e. B | A. x e. A ph } )
13	7 12	eqtrd	|- ( A = (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph } )
14		iinrab	|- ( A =/= (/) -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )
15	14	ineq1d	|- ( A =/= (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = ( { y e. B | A. x e. A ph } i^i B ) )
16		ssrab2	|- { y e. B | A. x e. A ph } C_ B
17		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 ) )
18	16 17	mpbi	|- { y e. B | A. x e. A ph } = ( { y e. B | A. x e. A ph } i^i B )
19	15 18	eqtr4di	|- ( A =/= (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph } )
20	13 19	pm2.61ine	|- ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph }