This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Extend wff notation to include the property 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 [ 𝑥 ⇄ 𝑦 ] 𝜑 |