This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iineq2d

Description: Equality deduction for indexed intersection. (Contributed by NM, 7-Dec-2011)

Ref Expression
Hypotheses iineq2d.1 ⊢ Ⅎ x φ
iineq2d.2 ⊢ φ ∧ x ∈ A → B = C
Assertion iineq2d ⊢ φ → ⋂ x ∈ A B = ⋂ x ∈ A C

Proof

Step Hyp Ref Expression
1 iineq2d.1 ⊢ Ⅎ x φ
2 iineq2d.2 ⊢ φ ∧ x ∈ A → B = C
3 2 ex ⊢ φ → x ∈ A → B = C
4 1 3 ralrimi ⊢ φ → ∀ x ∈ A B = C
5 iineq2 ⊢ ∀ x ∈ A B = C → ⋂ x ∈ A B = ⋂ x ∈ A C
6 4 5 syl ⊢ φ → ⋂ x ∈ A B = ⋂ x ∈ A C