Theorem eliind

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

	Ref	Expression
Hypotheses	eliind.a	⊢ ( 𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 )
	eliind.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
	eliind.d	⊢ ( 𝑥 = 𝐾 → ( 𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷 ) )
Assertion	eliind	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		eliind.a	⊢ ( 𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 )
2		eliind.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
3		eliind.d	⊢ ( 𝑥 = 𝐾 → ( 𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷 ) )
4		eliin	⊢ ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )
6	1 5	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 )
7	3 6 2	rspcdva	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )