Theorem sbal1
Check out sbal for a version not dependent on [ax-13]. A theorem
used in elimination of disjoint variable restriction on \( x \) and \( z \)
by replacing it with a distinctor \( \neg \forall x \, x = z \). (Contributed by
NM, 15-May-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2018.)
(New usage is discouraged.) (Proof modification is discouraged.)
Conclusion
\( \vdash \neg \forall x \, x = z \rightarrow ([ z / y ] \, \forall x \, \varphi \leftrightarrow \forall x \, [ z / y ] \, \varphi) \)
Proof
l0
sb4b
\( \vdash \neg \forall y \, y = z \rightarrow ([ z / y ] \, \forall x \, \varphi \leftrightarrow \forall y \, (y = z \rightarrow \forall x \, \varphi)) \)
l1
nfnae
l2
nfeqf2
\( \vdash \neg \forall x \, x = z \rightarrow \Finv x \, y = z \)
19.21t
bicomd _
\( \vdash \Finv x \, y = z \rightarrow (y = z \rightarrow \forall x \, \varphi \leftrightarrow \forall x \, (y = z \rightarrow \varphi)) \)
syl l2 _
albid l1 _
\( \vdash \neg \forall x \, x = z \rightarrow (\forall y \, (y = z \rightarrow \forall x \, \varphi) \leftrightarrow \forall y \, \forall x \, (y = z \rightarrow \varphi)) \)
l7
sylan9bbr l0 _
\( \vdash \neg \forall x \, x = z \wedge \neg \forall y \, y = z \rightarrow ([ z / y ] \, \forall x \, \varphi \leftrightarrow \forall y \, \forall x \, (y = z \rightarrow \varphi)) \)
l8
nfnae
sb4b
l10
albid l8 _
\( \vdash \neg \forall y \, y = z \rightarrow (\forall x \, [ z / y ] \, \varphi \leftrightarrow \forall x \, \forall y \, (y = z \rightarrow \varphi)) \)
alcom
\( \vdash \forall x \, \forall y \, (y = z \rightarrow \varphi) \leftrightarrow \forall y \, \forall x \, (y = z \rightarrow \varphi) \)
bitrdi l10 _
adantl _
\( \vdash \neg \forall x \, x = z \wedge \neg \forall y \, y = z \rightarrow (\forall x \, [ z / y ] \, \varphi \leftrightarrow \forall y \, \forall x \, (y = z \rightarrow \varphi)) \)
bitr4d l7 _
l15
ex _
\( \vdash \neg \forall x \, x = z \rightarrow \neg \forall y \, y = z \rightarrow ([ z / y ] \, \forall x \, \varphi \leftrightarrow \forall x \, [ z / y ] \, \varphi) \)
sbequ12
l17
sps _
\( \vdash \forall y \, y = z \rightarrow (\forall x \, \varphi \leftrightarrow [ z / y ] \, \forall x \, \varphi) \)
sbequ12
sps _
dral2 _
\( \vdash \forall y \, y = z \rightarrow (\forall x \, \varphi \leftrightarrow \forall x \, [ z / y ] \, \varphi) \)
bitr3d l17 _
\( \vdash \forall y \, y = z \rightarrow ([ z / y ] \, \forall x \, \varphi \leftrightarrow \forall x \, [ z / y ] \, \varphi) \)
pm2.61d2 l15 _