This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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