Definition df-ne

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

	Ref	Expression
Assertion	df-ne	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	wne	⊢ 𝐴 ≠ 𝐵
3	0 1	wceq	⊢ 𝐴 = 𝐵
4	3	wn	⊢ ¬ 𝐴 = 𝐵
5	2 4	wb	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )