An alternate definition of proper substitution [df-sb] that uses only
primitive connectives (no defined terms) on the right-hand side. Usage of
this theorem is discouraged because it depends on [ax-13]. (Contributed
by NM, 6-Mar-2007.) (New usage is discouraged.)
\( \vdash [ y' / x ] \, \varphi \leftrightarrow (x = y' \rightarrow \neg \varphi) \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
\( \vdash x = y' \wedge \varphi \vee \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \neg (x = y' \wedge \varphi) \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
\( \vdash [ y' / x ] \, \varphi \leftrightarrow x = y' \wedge \varphi \vee \forall x \, (x = y' \rightarrow \varphi) \)
\( \vdash (x = y' \rightarrow \neg \varphi) \rightarrow \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \neg (x = y' \wedge \varphi) \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)