Theorem nfsbd

Deduction version of nfsb. (Contributed by NM, 15-Feb-2013.) Usage of this theorem is discouraged because it depends on [ax-13]. Use nfsbv instead. (New usage is discouraged.)

Hypotheses
nfsbd.1
\( \vdash \Finv x \, \varphi \)
nfsbd.2
\( \vdash \varphi \rightarrow \Finv z \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv z \, [ y' / x ] \, \psi \)
Proof
l0
nfsbd.1
l1
nfsbd.2
l2
alrimi l0 _
\( \vdash \varphi \rightarrow \forall x \, \Finv z \, \psi \)
l3
nfsb4t
l4
syl l2 _
l5
cbvaev
\( \vdash \forall z \, z = y' \rightarrow \forall w \, w = y' \)
l6
axc16nf
\( \vdash \forall w \, w = y' \rightarrow \Finv z \, [ y' / x ] \, \psi \)
l7
syl l5 _
l8
pm2.61d2 l4 _