Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ceqsexv2d.1 | |
|
ceqsexv2d.2 | |
||
ceqsexv2d.3 | |
||
Assertion | ceqsexv2d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqsexv2d.1 | |
|
2 | ceqsexv2d.2 | |
|
3 | ceqsexv2d.3 | |
|
4 | 1 2 | ceqsexv | |
5 | 4 | biimpri | |
6 | exsimpr | |
|
7 | 3 5 6 | mp2b | |