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