Description: Extend wff definition to include proper substitution. Read: "the wff that results when y is properly substituted for x in wff ph ". (Contributed by NM, 24-Jan-2006)