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  5838  fiintim  7123  updjudhf  7278  netap  7473  elni2  7534  indpi  7562  nngt1ne1  9178  zapne  9554  prime  9579  elnn1uz2  9841  xrnemnf  10012  xrnepnf  10013  xaddcom  10096  xnegdi  10103  xpncan  10106  xleadd1a  10108  xsubge0  10116  flqeqceilz  10581  ndvdssub  12493  gcdsupex  12530  gcdsupcl  12531  gcdeq0  12550  gcd0id  12552  gcdmultiplez  12594  dvdssq  12604  algcvgblem  12623  lcmdvds  12653  lcmid  12654  mulgcddvds  12668  cncongr2  12678  isprm3  12692  isprm4  12693  sqrt2irr  12736  pcxcl  12886  isnzr2  14201  lgscllem  15739  umgr2edg1  16063  eupth2lem1  16312  eupth2lem3lem4fi  16327  bdne  16465  apdifflemr  16668