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	⊢ ( 𝐵 ≠ ∅ → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑥 𝐵
2	1	eliin2f	⊢ ( 𝐵 ≠ ∅ → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )