Definition df-ne 2403

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 2402	. 2 wff A =/= B
4	1, 2	wceq 1397	. . 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  2404  neir  2405  nner  2406  nnedc  2407  dcned  2408  neqned  2409  neirr  2411  eqneqall  2412  dcne  2413  nonconne  2414  neeq1  2415  neeq2  2416  neneqd  2423  necon3abii  2438  necon3bii  2440  necon3abid  2441  necon3bid  2443  necon3ad  2444  necon3bd  2445  necon3d  2446  necon3ai  2451  necon3bi  2452  necon1aidc  2453  necon1bidc  2454  necon1idc  2455  necon2ai  2456  necon2ad  2459  necon2bd  2460  necon2d  2461  necon1abiidc  2462  necon1bbiidc  2463  necon1abiddc  2464  necon1bbiddc  2465  necon4aidc  2470  necon4idc  2471  necon4addc  2472  necon4bddc  2473  necon4ddc  2474  necon4abiddc  2475  necon4biddc  2477  necon1addc  2478  necon1bddc  2479  necon1ddc  2480  neanior  2489  ne3anior  2490  nemtbir  2491  nfne  2495  nfned  2496  sbcne12g  3145  dfdif3  3317  ifnefalse  3616  opthpr  3855  prneimg  3857  exmid1dc  4290  exmid1stab  4298  onsucelsucexmid  4628  nnsuc  4714  ftpg  5839  fiintim  7126  updjudhf  7281  netap  7476  elni2  7537  indpi  7565  nngt1ne1  9181  zapne  9557  prime  9582  elnn1uz2  9844  xrnemnf  10015  xrnepnf  10016  xaddcom  10099  xnegdi  10106  xpncan  10109  xleadd1a  10111  xsubge0  10119  flqeqceilz  10584  ndvdssub  12512  gcdsupex  12549  gcdsupcl  12550  gcdeq0  12569  gcd0id  12571  gcdmultiplez  12613  dvdssq  12623  algcvgblem  12642  lcmdvds  12672  lcmid  12673  mulgcddvds  12687  cncongr2  12697  isprm3  12711  isprm4  12712  sqrt2irr  12755  pcxcl  12905  isnzr2  14220  lgscllem  15763  umgr2edg1  16087  eupth2lem1  16336  eupth2lem3lem4fi  16351  bdne  16507  apdifflemr  16710