Metamath Proof Explorer


Theorem ceqsexv2d

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025) (Proof shortened by SN, 5-Jun-2025)

Ref Expression
Hypotheses ceqsexv2d.1
|- A e. _V
ceqsexv2d.2
|- ( x = A -> ( ph <-> ps ) )
ceqsexv2d.3
|- ps
Assertion ceqsexv2d
|- E. x ph

Proof

Step Hyp Ref Expression
1 ceqsexv2d.1
 |-  A e. _V
2 ceqsexv2d.2
 |-  ( x = A -> ( ph <-> ps ) )
3 ceqsexv2d.3
 |-  ps
4 1 isseti
 |-  E. x x = A
5 3 2 mpbiri
 |-  ( x = A -> ph )
6 4 5 eximii
 |-  E. x ph