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 | |- ( x = A -> ( ph <-> ps ) ) |
|
| Assertion | ceqsexgv | |- ( A e. V -> ( E. x ( x = A /\ ph ) <-> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ceqsexgv.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
| 2 | id | |- ( x = A -> x = A ) |
|
| 3 | 2 1 | cgsexg | |- ( A e. V -> ( E. x ( x = A /\ ph ) <-> ps ) ) |