Description: Lemma used in proofs of implicit substitution properties. The converse
requires either a disjoint variable condition ( sb56 ) or a non-freeness
hypothesis ( equs45f ). Usage of this theorem is discouraged because it
depends on ax-13 . See equs4v for a weaker version requiring fewer
axioms. (Contributed by NM, 10-May-1993)(Proof shortened by Mario
Carneiro, 20-May-2014)(Proof shortened by Wolf Lammen, 5-Feb-2018)(New usage is discouraged.)