This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ne

Description: Define inequality. (Contributed by NM, 26-May-1993)

		Ref	Expression
	Assertion	df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2	0 1	wne	$wff A \neq B$
3	0 1	wceq	$wff A = B$
4	3	wn	$wff \neg A = B$
5	2 4	wb	$wff (A \neq B \leftrightarrow \neg A = B)$