Theorem iineq2

Description: Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	iineq2	|- ( A. x e. A B = C -> |^|_ x e. A B = |^|_ x e. A C )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( B = C -> ( y e. B <-> y e. C ) )
2	1	ralimi	|- ( A. x e. A B = C -> A. x e. A ( y e. B <-> y e. C ) )
3		ralbi	|- ( A. x e. A ( y e. B <-> y e. C ) -> ( A. x e. A y e. B <-> A. x e. A y e. C ) )
4	2 3	syl	|- ( A. x e. A B = C -> ( A. x e. A y e. B <-> A. x e. A y e. C ) )
5	4	abbidv	|- ( A. x e. A B = C -> { y | A. x e. A y e. B } = { y | A. x e. A y e. C } )
6		df-iin	|- |^|_ x e. A B = { y | A. x e. A y e. B }
7		df-iin	|- |^|_ x e. A C = { y | A. x e. A y e. C }
8	5 6 7	3eqtr4g	|- ( A. x e. A B = C -> |^|_ x e. A B = |^|_ x e. A C )