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 ∈ A B = C → ⋂ x ∈ A B = ⋂ x ∈ A C

Proof

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