Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996) Drop ax-10 and ax-12 . (Revised by Gino Giotto, 1-Dec-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ceqsexgv.1 | |
|
Assertion | ceqsexgv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqsexgv.1 | |
|
2 | id | |
|
3 | 2 1 | cgsexg | |