Definition df-ne

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	wne	$$wffA\ne B$$
3	0 1	wceq	$$wffA=B$$
4	3	wn	$$wff\neg A=B$$
5	2 4	wb	$$wff\left(A\ne B\leftrightarrow \neg A=B\right)$$