Theorem eliinid

Description: Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Assertion	eliinid	⊢ ( ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 )
2		eliin	⊢ ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )
3	2	adantr	⊢ ( ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )
4	1 3	mpbid	⊢ ( ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 )
5		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝐶 )
6	4 5	sylancom	⊢ ( ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝐶 )