Description: If z is not free in ph , it is not free in [ y / x ] ph when
y and z are distinct. Usage of this theorem is discouraged
because it depends on ax-13 . For a version requiring more disjoint
variables, but fewer axioms, see nfsbv . (Contributed by Mario
Carneiro, 11-Aug-2016)(Proof shortened by Wolf Lammen, 25-Feb-2024)(New usage is discouraged.)