Definition df-ne 2519

Description: Define inequality. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-ne	⊢ (A ≠ B ↔ ¬ A = B)

Detailed syntax breakdown of Definition df-ne

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wne 2517	. 2 wff A ≠ B
4	1, 2	wceq 1642	. . 3 wff A = B
5	4	wn 3	. 2 wff ¬ A = B
6	3, 5	wb 176	1 wff (A ≠ B ↔ ¬ A = B)

This definition is referenced by:  nne  2521  exmidne  2523  nonconne  2524  neeq1  2525  neeq2  2526  neneqd  2533  necon3abii  2547  necon3bii  2549  necon3abid  2550  necon3bid  2552  necon3d  2555  necon1ai  2559  necon1i  2561  necon2bd  2566  necon2d  2567  necon1abii  2568  necon1bbii  2569  necon1abid  2570  necon1bbid  2571  necon2abid  2574  necon2bbid  2575  necon4abid  2581  necon1ad  2584  neor  2601  neanior  2602  neorian  2604  nemtbir  2605  nfne  2611  nfned  2613  dfpss2  3355  ne0i  3557  neq0  3561  ab0  3570  ifnefalse  3671  eqsn  3868  snsssn  3874  unissint  3951  iununi  4051  0cnsuc  4402  nnsucelrlem2  4426  nnsucelrlem3  4427  nndisjeq  4430  preaddccan2lem1  4455  ltfinirr  4458  ltfinex  4465  ltfintrilem1  4466  tfinprop  4490  tfinltfin  4502  evenfinex  4504  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  evenodddisj  4517  sfinltfin  4536  vfinncvntnn  4549  vfinncvntsp  4550  nulnnn  4557  0cnelphi  4598  imasn  5019  xpcan  5058  xpcan2  5059  nfunv  5139  xpnedisj  5514  enprmaplem5  6081  fce  6189  el2c  6192  ncslemuc  6256  ncvsq  6257  0lt1c  6259  nnc3n3p1  6279  nchoicelem9  6298  nchoicelem12  6301  nchoicelem14  6303  fnfreclem2  6319  fnfreclem3  6320