Metamath Proof Explorer


Syntax definition wne

Description: Extend wff notation to include inequality.

Ref Expression
Assertion wne wff 𝐴𝐵