eliinid

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

		Ref	Expression
	Assertion	eliinid	$⊢ (A \in ⋂_{x \in B} C \land x \in B) \to A \in C$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ⋂_{x \in B} C \land x \in B) \to A \in ⋂_{x \in B} C$
2		eliin	$⊢ A \in ⋂_{x \in B} C \to (A \in ⋂_{x \in B} C \leftrightarrow \forall x \in B A \in C)$
3	2	adantr	$⊢ (A \in ⋂_{x \in B} C \land x \in B) \to (A \in ⋂_{x \in B} C \leftrightarrow \forall x \in B A \in C)$
4	1 3	mpbid	$⊢ (A \in ⋂_{x \in B} C \land x \in B) \to \forall x \in B A \in C$
5		rspa	$⊢ (\forall x \in B A \in C \land x \in B) \to A \in C$
6	4 5	sylancom	$⊢ (A \in ⋂_{x \in B} C \land x \in B) \to A \in C$

Metamath Proof Explorer