Metamath Proof Explorer

Theorem eliin2

Description: Membership in indexed intersection. See eliincex for a counterexample showing that the precondition B =/= (/) cannot be simply dropped. eliin uses an alternative precondition (and it doesn't have a disjoint var constraint between B and x ; see eliin2f ). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Assertion eliin2 ⊢ B ≠ ∅ → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ x B
2 1 eliin2f ⊢ B ≠ ∅ → A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C