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 ⊢∀x∈AB=C→⋂x∈AB=⋂x∈AC

Proof

Step Hyp Ref Expression
1 eleq2 ⊢B=C→y∈B↔y∈C
2 1 ralimi ⊢∀x∈AB=C→∀x∈Ay∈B↔y∈C
3 ralbi ⊢∀x∈Ay∈B↔y∈C→∀x∈Ay∈B↔∀x∈Ay∈C
4 2 3 syl ⊢∀x∈AB=C→∀x∈Ay∈B↔∀x∈Ay∈C
5 4 abbidv ⊢∀x∈AB=C→y|∀x∈Ay∈B=y|∀x∈Ay∈C
6 df-iin ⊢⋂x∈AB=y|∀x∈Ay∈B
7 df-iin ⊢⋂x∈AC=y|∀x∈Ay∈C
8 5 6 7 3eqtr4g ⊢∀x∈AB=C→⋂x∈AB=⋂x∈AC