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