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  3142  dfdif3  3314  ifnefalse  3613  opthpr  3850  prneimg  3852  exmid1dc  4284  exmid1stab  4292  onsucelsucexmid  4622  nnsuc  4708  ftpg  5823  fiintim  7093  updjudhf  7246  netap  7440  elni2  7501  indpi  7529  nngt1ne1  9145  zapne  9521  prime  9546  elnn1uz2  9802  xrnemnf  9973  xrnepnf  9974  xaddcom  10057  xnegdi  10064  xpncan  10067  xleadd1a  10069  xsubge0  10077  flqeqceilz  10540  ndvdssub  12441  gcdsupex  12478  gcdsupcl  12479  gcdeq0  12498  gcd0id  12500  gcdmultiplez  12542  dvdssq  12552  algcvgblem  12571  lcmdvds  12601  lcmid  12602  mulgcddvds  12616  cncongr2  12626  isprm3  12640  isprm4  12641  sqrt2irr  12684  pcxcl  12834  isnzr2  14148  lgscllem  15686  umgr2edg1  16007  bdne  16216  apdifflemr  16415