# Metamath Proof Explorer

## Theorem ceqsex

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995) (Revised by Mario Carneiro, 10-Oct-2016)

Ref Expression
Hypotheses ceqsex.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
ceqsex.2 ${⊢}{A}\in \mathrm{V}$
ceqsex.3 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
Assertion ceqsex ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\phi }\right)↔{\psi }$

### Proof

Step Hyp Ref Expression
1 ceqsex.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 ceqsex.2 ${⊢}{A}\in \mathrm{V}$
3 ceqsex.3 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
4 3 biimpa ${⊢}\left({x}={A}\wedge {\phi }\right)\to {\psi }$
5 1 4 exlimi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\phi }\right)\to {\psi }$
6 3 biimprcd ${⊢}{\psi }\to \left({x}={A}\to {\phi }\right)$
7 1 6 alrimi ${⊢}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {\phi }\right)$
8 2 isseti ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
9 exintr ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\phi }\right)\right)$
10 7 8 9 mpisyl ${⊢}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\phi }\right)$
11 5 10 impbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {\phi }\right)↔{\psi }$