Syntax definition wich

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 ".

	Ref	Expression
Assertion	wich	$$wff\left[x\rightleftarrows y\right]\phi$$