Description: A lemma for substitutions, proved from Tarski's FOL. The version without
DV ( x , y ) is true but requires ax-13 . The disjoint variable
condition DV ( x , ph ) is necessary for both directions: consider
substituting x = z for ph . (Contributed by BJ, 25-May-2021)