Metamath Proof Explorer


Theorem ceqsexv

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995)

Ref Expression
Hypotheses ceqsexv.1 𝐴 ∈ V
ceqsexv.2 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
Assertion ceqsexv ( ∃ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ 𝜓 )

Proof

Step Hyp Ref Expression
1 ceqsexv.1 𝐴 ∈ V
2 ceqsexv.2 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
3 nfv 𝑥 𝜓
4 3 1 2 ceqsex ( ∃ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ 𝜓 )