Metamath Proof Explorer


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 x y φ