Syntax Definition wne 1190

Description: Extend wff notation to include inequality.

Hypotheses

Ref	Expression
cA	class A
cB	class B

Assertion

Ref	Expression
wne	wff A ≠ B

See definition df-ne 1192 for more information.

metamath.org