Description: This version of dfsb7 does not require that ph and z be
distinct. 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 doesn't have the concept of a variable not occurring in a wff.
( 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)(Proof shortened by Andrew Salmon, 25-May-2011)(New usage is discouraged.)