Metamath Proof Explorer

Theorem equsexvwOLD

Description: Obsolete version of equsexvw as of 23-Oct-2023. (Contributed by BJ, 31-May-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis equsalvw.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion equsexvwOLD ${⊢}\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 1 pm5.32i ${⊢}\left({x}={y}\wedge {\phi }\right)↔\left({x}={y}\wedge {\psi }\right)$
3 2 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)$
4 ax6ev ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
5 19.41v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge {\psi }\right)$
6 4 5 mpbiran ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\psi }\right)↔{\psi }$
7 3 6 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔{\psi }$