# Metamath Proof Explorer

## Theorem equsexALT

Description: Alternate proof of equsex . This proves the result directly, instead of as a corollary of equsal via equs4 . Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 is ax6e . This proof mimics that of equsal (in particular, note that pm5.32i , exbii , 19.41 , mpbiran correspond respectively to pm5.74i , albii , 19.23 , a1bi ). (Contributed by BJ, 20-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses equsal.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
equsal.2 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion equsexALT ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔{\psi }$

### Proof

Step Hyp Ref Expression
1 equsal.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 equsal.2 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
3 2 pm5.32i ${⊢}\left({x}={y}\wedge {\phi }\right)↔\left({x}={y}\wedge {\psi }\right)$
4 3 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\psi }\right)$
5 ax6e ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
6 1 19.41 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge {\psi }\right)$
7 5 6 mpbiran ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\psi }\right)↔{\psi }$
8 4 7 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔{\psi }$