Description: Implicit substitution of y for x into a theorem. Usage of this
theorem is discouraged because it depends on ax-13 . Use the weaker
chvarvv if possible. (Contributed by NM, 20-Apr-1994)(Proof
shortened by Wolf Lammen, 22-Apr-2018)(New usage is discouraged.)