# Metamath Proof Explorer

## Theorem equsexvw

Description: Version of equsexv with a disjoint variable condition, and of equsex with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw . (Contributed by BJ, 31-May-2019) (Proof shortened by Wolf Lammen, 23-Oct-2023)

Ref Expression
Hypothesis equsalvw.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion equsexvw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔{\psi }$

### Proof

Step Hyp Ref Expression
1 equsalvw.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 alinexa ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)$
3 1 notbid ${⊢}{x}={y}\to \left(¬{\phi }↔¬{\psi }\right)$
4 3 equsalvw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)↔¬{\psi }$
5 2 4 bitr3i ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔¬{\psi }$
6 5 con4bii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔{\psi }$