Definition df-ne 2401

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 2400	. 2 wff A =/= B
4	1, 2	wceq 1395	. . 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  2402  neir  2403  nner  2404  nnedc  2405  dcned  2406  neqned  2407  neirr  2409  eqneqall  2410  dcne  2411  nonconne  2412  neeq1  2413  neeq2  2414  neneqd  2421  necon3abii  2436  necon3bii  2438  necon3abid  2439  necon3bid  2441  necon3ad  2442  necon3bd  2443  necon3d  2444  necon3ai  2449  necon3bi  2450  necon1aidc  2451  necon1bidc  2452  necon1idc  2453  necon2ai  2454  necon2ad  2457  necon2bd  2458  necon2d  2459  necon1abiidc  2460  necon1bbiidc  2461  necon1abiddc  2462  necon1bbiddc  2463  necon4aidc  2468  necon4idc  2469  necon4addc  2470  necon4bddc  2471  necon4ddc  2472  necon4abiddc  2473  necon4biddc  2475  necon1addc  2476  necon1bddc  2477  necon1ddc  2478  neanior  2487  ne3anior  2488  nemtbir  2489  nfne  2493  nfned  2494  sbcne12g  3143  dfdif3  3315  ifnefalse  3614  opthpr  3853  prneimg  3855  exmid1dc  4288  exmid1stab  4296  onsucelsucexmid  4626  nnsuc  4712  ftpg  5833  fiintim  7118  updjudhf  7272  netap  7466  elni2  7527  indpi  7555  nngt1ne1  9171  zapne  9547  prime  9572  elnn1uz2  9834  xrnemnf  10005  xrnepnf  10006  xaddcom  10089  xnegdi  10096  xpncan  10099  xleadd1a  10101  xsubge0  10109  flqeqceilz  10573  ndvdssub  12484  gcdsupex  12521  gcdsupcl  12522  gcdeq0  12541  gcd0id  12543  gcdmultiplez  12585  dvdssq  12595  algcvgblem  12614  lcmdvds  12644  lcmid  12645  mulgcddvds  12659  cncongr2  12669  isprm3  12683  isprm4  12684  sqrt2irr  12727  pcxcl  12877  isnzr2  14191  lgscllem  15729  umgr2edg1  16053  bdne  16398  apdifflemr  16601