Description: Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999) (Proof shortened by Wolf Lammen, 12-Jan-2025)