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 V
ceqsexv2d.2 x = A φ ψ
ceqsexv2d.3 ψ
Assertion ceqsexv2d x φ

Proof

Step Hyp Ref Expression
1 ceqsexv2d.1 A V
2 ceqsexv2d.2 x = A φ ψ
3 ceqsexv2d.3 ψ
4 1 isseti x x = A
5 3 2 mpbiri x = A φ
6 4 5 eximii x φ