This version of dfsb7 does not require that \( \varphi \) 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.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.)