Theorem nfsb4t
A variable not free in a proposition remains so after substitution in that
proposition with a distinct variable (closed form of nfsb4 ). Usage of
this theorem is discouraged because it depends on [ax-13]. (Contributed
by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof
shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
Conclusion
\( \vdash \forall x \, \Finv z \, \varphi \rightarrow \neg \forall z \, z = y' \rightarrow \Finv z \, [ y' / x ] \, \varphi \)
Proof
l0
nfv
\( \vdash \Finv z \, x = w \)
l1
a1i _
\( \vdash \forall x \, \Finv z \, \varphi \rightarrow \Finv z \, x = w \)
l2
sp
\( \vdash \forall x \, \Finv z \, \varphi \rightarrow \Finv z \, \varphi \)
l3
nfimd l1 _
l4
nfa1
\( \vdash \Finv x \, \forall x \, \Finv z \, \varphi \)
l5
nfald l4 l3
\( \vdash \forall x \, \Finv z \, \varphi \rightarrow \Finv z \, \forall x \, (x = w \rightarrow \varphi) \)
l6
nfeqf
\( \vdash \neg \forall z \, z = w \wedge \neg \forall z \, z = y' \rightarrow \Finv z \, w = y' \)
l7
ex _
l8
com12 _
\( \vdash \neg \forall z \, z = y' \rightarrow \neg \forall z \, z = w \rightarrow \Finv z \, w = y' \)
l9
cbvaev
\( \vdash \forall z \, z = w \rightarrow \forall v \, v = w \)
l10
axc16nf
\( \vdash \forall v \, v = w \rightarrow \Finv z \, w = y' \)
l11
syl l9 _
l12
pm2.61d2 l8 _
l13
adantl _
\( \vdash \forall x \, \Finv z \, \varphi \wedge \neg \forall z \, z = y' \rightarrow \Finv z \, w = y' \)
l14
adantr l5
\( \vdash \forall x \, \Finv z \, \varphi \wedge \neg \forall z \, z = y' \rightarrow \Finv z \, \forall x \, (x = w \rightarrow \varphi) \)
l15
nfimd l13 _
l16
nfv
\( \vdash \Finv w \, (\forall x \, \Finv z \, \varphi \wedge \neg \forall z \, z = y') \)
l17
nfald _ l15
\( \vdash \forall x \, \Finv z \, \varphi \wedge \neg \forall z \, z = y' \rightarrow \Finv z \, \forall w \, (w = y' \rightarrow \forall x \, (x = w \rightarrow \varphi)) \)
l18
dfsb
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \forall w \, (w = y' \rightarrow \forall x \, (x = w \rightarrow \varphi)) \)
l19
nfbii _
l20
sylibr l17 _
l21
ex _