Description: Substitution applied to an atomic wff (class version of equsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010)