Theorem dfsb2
An alternate definition of proper substitution that, like dfsb1, mixes
free and bound variables to avoid distinct variable requirements. Usage
of this theorem is discouraged because it depends on [ax-13].
(Contributed by NM, 17-Feb-2005.) (New usage is discouraged.)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow x = y' \wedge \varphi \vee \forall x \, (x = y' \rightarrow \varphi) \)
Proof
l0
sp
\( \vdash \forall x \, x = y' \rightarrow x = y' \)
sbequ2
l2
sps _
\( \vdash \forall x \, x = y' \rightarrow [ y' / x ] \, \varphi \rightarrow \varphi \)
orc
\( \vdash x = y' \wedge \varphi \rightarrow x = y' \wedge \varphi \vee \forall x \, (x = y' \rightarrow \varphi) \)
l4
syl6an l0 l2 _
\( \vdash \forall x \, x = y' \rightarrow [ y' / x ] \, \varphi \rightarrow x = y' \wedge \varphi \vee \forall x \, (x = y' \rightarrow \varphi) \)
l5
sb4b
\( \vdash \neg \forall x \, x = y' \rightarrow ([ y' / x ] \, \varphi \leftrightarrow \forall x \, (x = y' \rightarrow \varphi)) \)
olc
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow x = y' \wedge \varphi \vee \forall x \, (x = y' \rightarrow \varphi) \)
biimtrdi l5 _
\( \vdash \neg \forall x \, x = y' \rightarrow [ y' / x ] \, \varphi \rightarrow x = y' \wedge \varphi \vee \forall x \, (x = y' \rightarrow \varphi) \)
l8
pm2.61i l4 _
sbequ1
l10
imp _
sb2
jaoi l10 _
impbii l8 _