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

Metamath Proof Explorer

Theorem eliind

Description: Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses eliind.a ⊢ φ → A ∈ ⋂ x ∈ B C
eliind.k ⊢ φ → K ∈ B
eliind.d ⊢ x = K → A ∈ C ↔ A ∈ D
Assertion eliind ⊢ φ → A ∈ D

Proof

Step Hyp Ref Expression
1 eliind.a ⊢ φ → A ∈ ⋂ x ∈ B C
2 eliind.k ⊢ φ → K ∈ B
3 eliind.d ⊢ x = K → A ∈ C ↔ A ∈ D
4 eliin ⊢ A ∈ ⋂ x ∈ B C → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C
5 1 4 syl ⊢ φ → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C
6 1 5 mpbid ⊢ φ → ∀ x ∈ B A ∈ C
7 3 6 2 rspcdva ⊢ φ → A ∈ D