Theorem dfsb1

Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before [df-sb]. Note that it does not require dummy variables in its definiens; this is done by having \( x \) free in the first conjunct and bound in the second. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by BJ, 9-Jul-2023.) Revise [df-sb]. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.)

Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow (x = y' \rightarrow \varphi) \wedge \exists x \, (x = y' \wedge \varphi) \)
Proof
sbequ2
l1
com12 _
sb1
l3
jca l1 _
l4
id
sbequ1
embantd l4 _
sps _
l8
adantrd _
\( \vdash \forall x \, x = y' \rightarrow (x = y' \rightarrow \varphi) \wedge \exists x \, (x = y' \wedge \varphi) \rightarrow [ y' / x ] \, \varphi \)
sb3
adantld _
\( \vdash \neg \forall x \, x = y' \rightarrow (x = y' \rightarrow \varphi) \wedge \exists x \, (x = y' \wedge \varphi) \rightarrow [ y' / x ] \, \varphi \)
pm2.61i l8 _
impbii l3 _