Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993) (Proof shortened by Andrew Salmon, 25-May-2011)