Theorem equs5

Lemma used in proofs of substitution properties. If there is a disjoint variable condition on x , y, then sbalex can be used instead; if \( y' \) is not free in \( \varphi \), 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.)

Conclusion
\( \vdash \neg \forall x \, x = y' \rightarrow (\exists x \, (x = y' \wedge \varphi) \leftrightarrow \forall x \, (x = y' \rightarrow \varphi)) \)
Proof
l0
nfna1
l1
nfa1
axc15
impd _
l4
exlimd l0 l1 _
equs4
impbid1 l4 _