Description: Extend wff notation to include the proper substitution of a class for a set. Read this notation as "the proper substitution of class A for setvar variable x in wff ph ".
wff [. A / x ]. ph