Description: Extend wff notation to include the propery of a wff ph that the setvar variables x and y are interchangeable. Read this notation as " x and y are interchangeable in wff ph ".
wff [ x <> y ] ph