Description: 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.)