Metamath Proof Explorer


Theorem iineq12f

Description: Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Hypotheses iineq12f.1
|- F/_ x A
iineq12f.2
|- F/_ x B
Assertion iineq12f
|- ( ( A = B /\ A. x e. A C = D ) -> |^|_ x e. A C = |^|_ x e. B D )

Proof

Step Hyp Ref Expression
1 iineq12f.1
 |-  F/_ x A
2 iineq12f.2
 |-  F/_ x B
3 eleq2
 |-  ( C = D -> ( y e. C <-> y e. D ) )
4 3 ralimi
 |-  ( A. x e. A C = D -> A. x e. A ( y e. C <-> y e. D ) )
5 ralbi
 |-  ( A. x e. A ( y e. C <-> y e. D ) -> ( A. x e. A y e. C <-> A. x e. A y e. D ) )
6 4 5 syl
 |-  ( A. x e. A C = D -> ( A. x e. A y e. C <-> A. x e. A y e. D ) )
7 1 2 raleqf
 |-  ( A = B -> ( A. x e. A y e. D <-> A. x e. B y e. D ) )
8 6 7 sylan9bbr
 |-  ( ( A = B /\ A. x e. A C = D ) -> ( A. x e. A y e. C <-> A. x e. B y e. D ) )
9 8 abbidv
 |-  ( ( A = B /\ A. x e. A C = D ) -> { y | A. x e. A y e. C } = { y | A. x e. B y e. D } )
10 df-iin
 |-  |^|_ x e. A C = { y | A. x e. A y e. C }
11 df-iin
 |-  |^|_ x e. B D = { y | A. x e. B y e. D }
12 9 10 11 3eqtr4g
 |-  ( ( A = B /\ A. x e. A C = D ) -> |^|_ x e. A C = |^|_ x e. B D )