Simplified definition of substitution when variables are distinct. This
is the biconditional strengthening of sb3. Usage of this theorem is
discouraged because it depends on [ax-13]. (Contributed by BJ,
6-Oct-2018.) Shorten sb3. (Revised by Wolf Lammen, 21-Feb-2021.)
(New usage is discouraged.)
\( \vdash \neg \forall x \, x = y' \rightarrow ([ y' / x ] \, \varphi \leftrightarrow \exists x \, (x = y' \wedge \varphi)) \)
\( \vdash \neg \forall x \, x = y' \rightarrow ([ y' / x ] \, \varphi \leftrightarrow \forall x \, (x = y' \rightarrow \varphi)) \)
\( \vdash \neg \forall x \, x = y' \rightarrow (\exists x \, (x = y' \wedge \varphi) \leftrightarrow \forall x \, (x = y' \rightarrow \varphi)) \)