Theorem cpcoll2d

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

	Ref	Expression
Hypotheses	cpcoll2d.1	$$⊢\phi \to x\in A$$
	cpcoll2d.2	$$⊢\phi \to \exists yxFy$$
Assertion	cpcoll2d	$$⊢\phi \to \exists y\in \left(FCollA\right)xFy$$

Proof

Step	Hyp	Ref	Expression
1		cpcoll2d.1	$$⊢\phi \to x\in A$$
2		cpcoll2d.2	$$⊢\phi \to \exists yxFy$$
3		breq2	$$⊢a=y\to \left(xFa\leftrightarrow xFy\right)$$
4	3	cbvexvw	$$⊢\exists axFa\leftrightarrow \exists yxFy$$
5	2 4	sylibr	$$⊢\phi \to \exists axFa$$
6	1	adantr	$$⊢\left(\phi \wedge xFa\right)\to x\in A$$
7		simpr	$$⊢\left(\phi \wedge xFa\right)\to xFa$$
8	6 7	cpcolld	$$⊢\left(\phi \wedge xFa\right)\to \exists a\in \left(FCollA\right)xFa$$
9	3	cbvrexvw	$$⊢\exists a\in \left(FCollA\right)xFa\leftrightarrow \exists y\in \left(FCollA\right)xFy$$
10	8 9	sylib	$$⊢\left(\phi \wedge xFa\right)\to \exists y\in \left(FCollA\right)xFy$$
11	5 10	exlimddv	$$⊢\phi \to \exists y\in \left(FCollA\right)xFy$$