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	|- ( ( A e. |^|_ x e. B C /\ x e. B ) -> A e. C )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. |^|_ x e. B C /\ x e. B ) -> A e. |^|_ x e. B C )
2		eliin	|- ( A e. |^|_ x e. B C -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
3	2	adantr	|- ( ( A e. |^|_ x e. B C /\ x e. B ) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
4	1 3	mpbid	|- ( ( A e. |^|_ x e. B C /\ x e. B ) -> A. x e. B A e. C )
5		rspa	|- ( ( A. x e. B A e. C /\ x e. B ) -> A e. C )
6	4 5	sylancom	|- ( ( A e. |^|_ x e. B C /\ x e. B ) -> A e. C )