Metamath Proof Explorer


Theorem ceqsexv2d

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016)

Ref Expression
Hypotheses ceqsexv2d.1 AV
ceqsexv2d.2 x=Aφψ
ceqsexv2d.3 ψ
Assertion ceqsexv2d xφ

Proof

Step Hyp Ref Expression
1 ceqsexv2d.1 AV
2 ceqsexv2d.2 x=Aφψ
3 ceqsexv2d.3 ψ
4 1 2 ceqsexv xx=Aφψ
5 4 biimpri ψxx=Aφ
6 exsimpr xx=Aφxφ
7 3 5 6 mp2b xφ