Theorem eliind2

Description: Membership in indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	eliind2.1	|- F/ x ph
	eliind2.2	|- ( ph -> A e. V )
	eliind2.3	|- ( ( ph /\ x e. B ) -> A e. C )
Assertion	eliind2	|- ( ph -> A e. |^|_ x e. B C )

Proof

Step	Hyp	Ref	Expression
1		eliind2.1	|- F/ x ph
2		eliind2.2	|- ( ph -> A e. V )
3		eliind2.3	|- ( ( ph /\ x e. B ) -> A e. C )
4	3	ex	|- ( ph -> ( x e. B -> A e. C ) )
5	1 4	ralrimi	|- ( ph -> A. x e. B A e. C )
6		eliin	|- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
7	2 6	syl	|- ( ph -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
8	5 7	mpbird	|- ( ph -> A e. |^|_ x e. B C )