Description: This version of dfsb7 does not require that ph and z be
disjoint. This permits it to be used as a definition for substitution
in a formalization that omits the logically redundant axiom ax-5 ,
i.e., that does not have the concept of a variable not occurring in a
formula. (Definition dfsb1 is also suitable, but its mixing of free
and bound variables is distasteful to some logicians.) Usage of this
theorem is discouraged because it depends on ax-13 . (Contributed by NM, 26-Jul-2006)(Revised by Mario Carneiro, 6-Oct-2016)(New usage is discouraged.)