Description: cpcolld with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cpcoll2d.1 | ||
cpcoll2d.2 | |||
Assertion | cpcoll2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpcoll2d.1 | ||
2 | cpcoll2d.2 | ||
3 | breq2 | ||
4 | 3 | cbvexvw | |
5 | 2 4 | sylibr | |
6 | 1 | adantr | |
7 | simpr | ||
8 | 6 7 | cpcolld | |
9 | 3 | cbvrexvw | |
10 | 8 9 | sylib | |
11 | 5 10 | exlimddv |