Metamath Proof Explorer


Theorem iineq12f

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

Ref Expression
Hypotheses iineq12f.1 _ x A
iineq12f.2 _ x B
Assertion iineq12f A = B x A C = D x A C = x B D

Proof

Step Hyp Ref Expression
1 iineq12f.1 _ x A
2 iineq12f.2 _ x B
3 eleq2 C = D y C y D
4 3 ralimi x A C = D x A y C y D
5 ralbi x A y C y D x A y C x A y D
6 4 5 syl x A C = D x A y C x A y D
7 1 2 raleqf A = B x A y D x B y D
8 6 7 sylan9bbr A = B x A C = D x A y C x B y D
9 8 abbidv A = B x A C = D y | x A y C = y | x B y D
10 df-iin x A C = y | x A y C
11 df-iin x B D = y | x B y D
12 9 10 11 3eqtr4g A = B x A C = D x A C = x B D