# Metamath Proof Explorer

## Theorem equs5

Description: Lemma used in proofs of substitution properties. If there is a disjoint variable condition on x , y , then sb56 can be used instead; if y is not free in ph , then equs45f can be used. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 14-May-1993) (Revised by BJ, 1-Oct-2018) (New usage is discouraged.)

Ref Expression
Assertion equs5 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 nfna1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
2 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$
3 axc15 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\right)$
4 3 impd ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\left({x}={y}\wedge {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)$
5 1 2 4 exlimd ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)$
6 equs4 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)$
7 5 6 impbid1 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)$