Definition df-ne

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

	Ref	Expression
Assertion	df-ne	|- ( A =/= B <-> -. A = B )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	wne	|- A =/= B
3	0 1	wceq	|- A = B
4	3	wn	|- -. A = B
5	2 4	wb	|- ( A =/= B <-> -. A = B )