Metamath Proof Explorer

Theorem eliin

Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion eliin ⊢ A ∈ V → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ y = A → y ∈ C ↔ A ∈ C
2 1 ralbidv ⊢ y = A → ∀ x ∈ B y ∈ C ↔ ∀ x ∈ B A ∈ C
3 df-iin ⊢ ⋂ x ∈ B C = y | ∀ x ∈ B y ∈ C
4 2 3 elab2g ⊢ A ∈ V → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C