Theorem nfsb4

A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (inference associated with nfsb4t ). Theorem nfsb replaces the distinctor antecedent with a disjoint variable condition. See nfsbv for a weaker version of nfsb not requiring [ax-13]. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on [ax-13]. Use nfsbv instead. (New usage is discouraged.)

Hypothesis
nfsb4.1
\( \vdash \Finv z \, \varphi \)
Conclusion
\( \vdash \neg \forall z \, z = y' \rightarrow \Finv z \, [ y' / x ] \, \varphi \)
Proof
l0
nfsb4t
\( \vdash \forall x \, \Finv z \, \varphi \rightarrow \neg \forall z \, z = y' \rightarrow \Finv z \, [ y' / x ] \, \varphi \)
nfsb4.1
\( \vdash \Finv z \, \varphi \)
mpg l0 _