Description: A property related to substitution that unlike equs5 does not require a
distinctor antecedent. This proof uses ax12 , see equs5eALT for an
alternative one using ax-12 but not ax13 . Usage of this theorem is
discouraged because it depends on ax-13 . (Contributed by NM, 2-Feb-2007)(Proof shortened by Wolf Lammen, 15-Jan-2018)(New usage is discouraged.)