This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )