Theorem iineq1

Description: Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998)

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

Proof

Step	Hyp	Ref	Expression
1		raleq	|- ( A = B -> ( A. x e. A y e. C <-> A. x e. B y e. C ) )
2	1	abbidv	|- ( A = B -> { y | A. x e. A y e. C } = { y | A. x e. B y e. C } )
3		df-iin	|- |^|_ x e. A C = { y | A. x e. A y e. C }
4		df-iin	|- |^|_ x e. B C = { y | A. x e. B y e. C }
5	2 3 4	3eqtr4g	|- ( A = B -> |^|_ x e. A C = |^|_ x e. B C )