Theorem iinrab

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

	Ref	Expression
Assertion	iinrab	|- ( A =/= (/) -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )

Proof

Step	Hyp	Ref	Expression
1		r19.28zv	|- ( A =/= (/) -> ( A. x e. A ( y e. B /\ ph ) <-> ( y e. B /\ A. x e. A ph ) ) )
2	1	abbidv	|- ( A =/= (/) -> { y | A. x e. A ( y e. B /\ ph ) } = { y | ( y e. B /\ A. x e. A ph ) } )
3		df-rab	|- { y e. B | ph } = { y | ( y e. B /\ ph ) }
4	3	a1i	|- ( x e. A -> { y e. B | ph } = { y | ( y e. B /\ ph ) } )
5	4	iineq2i	|- |^|_ x e. A { y e. B | ph } = |^|_ x e. A { y | ( y e. B /\ ph ) }
6		iinab	|- |^|_ x e. A { y | ( y e. B /\ ph ) } = { y | A. x e. A ( y e. B /\ ph ) }
7	5 6	eqtri	|- |^|_ x e. A { y e. B | ph } = { y | A. x e. A ( y e. B /\ ph ) }
8		df-rab	|- { y e. B | A. x e. A ph } = { y | ( y e. B /\ A. x e. A ph ) }
9	2 7 8	3eqtr4g	|- ( A =/= (/) -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )