# Metamath Proof Explorer

## Theorem equsexv

Description: An equivalence related to implicit substitution. Version of equsex with a disjoint variable condition, which does not require ax-13 . See equsexvw for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv . (Contributed by NM, 5-Aug-1993) (Revised by BJ, 31-May-2019)

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

### Proof

Step Hyp Ref Expression
1 equsalv.nf ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 equsalv.1 ${⊢}{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 ax6ev ${⊢}\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 }$