Theorem eliind

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

	Ref	Expression
Hypotheses	eliind.a	|- ( ph -> A e. |^|_ x e. B C )
	eliind.k	|- ( ph -> K e. B )
	eliind.d	|- ( x = K -> ( A e. C <-> A e. D ) )
Assertion	eliind	|- ( ph -> A e. D )

Proof

Step	Hyp	Ref	Expression
1		eliind.a	|- ( ph -> A e. |^|_ x e. B C )
2		eliind.k	|- ( ph -> K e. B )
3		eliind.d	|- ( x = K -> ( A e. C <-> A e. D ) )
4		eliin	|- ( A e. |^|_ x e. B C -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
5	1 4	syl	|- ( ph -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
6	1 5	mpbid	|- ( ph -> A. x e. B A e. C )
7	3 6 2	rspcdva	|- ( ph -> A e. D )