Theorem cpcoll2d

Description: cpcolld with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023)

	Ref	Expression
Hypotheses	cpcoll2d.1	|- ( ph -> x e. A )
	cpcoll2d.2	|- ( ph -> E. y x F y )
Assertion	cpcoll2d	|- ( ph -> E. y e. ( F Coll A ) x F y )

Proof

Step	Hyp	Ref	Expression
1		cpcoll2d.1	|- ( ph -> x e. A )
2		cpcoll2d.2	|- ( ph -> E. y x F y )
3		breq2	|- ( a = y -> ( x F a <-> x F y ) )
4	3	cbvexvw	|- ( E. a x F a <-> E. y x F y )
5	2 4	sylibr	|- ( ph -> E. a x F a )
6	1	adantr	|- ( ( ph /\ x F a ) -> x e. A )
7		simpr	|- ( ( ph /\ x F a ) -> x F a )
8	6 7	cpcolld	|- ( ( ph /\ x F a ) -> E. a e. ( F Coll A ) x F a )
9	3	cbvrexvw	|- ( E. a e. ( F Coll A ) x F a <-> E. y e. ( F Coll A ) x F y )
10	8 9	sylib	|- ( ( ph /\ x F a ) -> E. y e. ( F Coll A ) x F y )
11	5 10	exlimddv	|- ( ph -> E. y e. ( F Coll A ) x F y )