Description: An equivalence related to implicit substitution. Usage of this theorem
is discouraged because it depends on ax-13 . See equsalhw for a
version with a disjoint variable condition requiring fewer axioms.
(Contributed by NM, 2-Jun-1993)(New usage is discouraged.)