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 𝐴 ∈ V
ceqsexv2d.2 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
ceqsexv2d.3 𝜓
Assertion ceqsexv2d 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 ceqsexv2d.1 𝐴 ∈ V
2 ceqsexv2d.2 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
3 ceqsexv2d.3 𝜓
4 1 isseti 𝑥 𝑥 = 𝐴
5 3 2 mpbiri ( 𝑥 = 𝐴𝜑 )
6 4 5 eximii 𝑥 𝜑