Definition df-ne 2368

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 2367	. 2 wff A =/= B
4	1, 2	wceq 1364	. . 3 wff A = B
5	4	wn 3	. 2 wff -. A = B
6	3, 5	wb 105	1 wff ( A =/= B <-> -. A = B )

This definition is referenced by:  neii  2369  neir  2370  nner  2371  nnedc  2372  dcned  2373  neqned  2374  neirr  2376  eqneqall  2377  dcne  2378  nonconne  2379  neeq1  2380  neeq2  2381  neneqd  2388  necon3abii  2403  necon3bii  2405  necon3abid  2406  necon3bid  2408  necon3ad  2409  necon3bd  2410  necon3d  2411  necon3ai  2416  necon3bi  2417  necon1aidc  2418  necon1bidc  2419  necon1idc  2420  necon2ai  2421  necon2ad  2424  necon2bd  2425  necon2d  2426  necon1abiidc  2427  necon1bbiidc  2428  necon1abiddc  2429  necon1bbiddc  2430  necon4aidc  2435  necon4idc  2436  necon4addc  2437  necon4bddc  2438  necon4ddc  2439  necon4abiddc  2440  necon4biddc  2442  necon1addc  2443  necon1bddc  2444  necon1ddc  2445  neanior  2454  ne3anior  2455  nemtbir  2456  nfne  2460  nfned  2461  sbcne12g  3102  dfdif3  3274  ifnefalse  3573  opthpr  3803  prneimg  3805  exmid1dc  4234  exmid1stab  4242  onsucelsucexmid  4567  nnsuc  4653  ftpg  5749  fiintim  7001  updjudhf  7154  netap  7337  elni2  7398  indpi  7426  nngt1ne1  9042  zapne  9417  prime  9442  elnn1uz2  9698  xrnemnf  9869  xrnepnf  9870  xaddcom  9953  xnegdi  9960  xpncan  9963  xleadd1a  9965  xsubge0  9973  flqeqceilz  10427  ndvdssub  12112  gcdsupex  12149  gcdsupcl  12150  gcdeq0  12169  gcd0id  12171  gcdmultiplez  12213  dvdssq  12223  algcvgblem  12242  lcmdvds  12272  lcmid  12273  mulgcddvds  12287  cncongr2  12297  isprm3  12311  isprm4  12312  sqrt2irr  12355  pcxcl  12505  isnzr2  13816  lgscllem  15332  bdne  15583  apdifflemr  15778