Metamath Proof Explorer


Theorem cpcoll2d

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

Ref Expression
Hypotheses cpcoll2d.1 φ x A
cpcoll2d.2 φ y x F y
Assertion cpcoll2d φ y F Coll A x F y

Proof

Step Hyp Ref Expression
1 cpcoll2d.1 φ x A
2 cpcoll2d.2 φ y x F y
3 breq2 a = y x F a x F y
4 3 cbvexvw a x F a y x F y
5 2 4 sylibr φ a x F a
6 1 adantr φ x F a x A
7 simpr φ x F a x F a
8 6 7 cpcolld φ x F a a F Coll A x F a
9 3 cbvrexvw a F Coll A x F a y F Coll A x F y
10 8 9 sylib φ x F a y F Coll A x F y
11 5 10 exlimddv φ y F Coll A x F y