Definition df-ne 2415

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 2414	. 2 wff A =/= B
4	1, 2	wceq 1398	. . 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  2416  neir  2417  nner  2418  nnedc  2419  dcned  2420  neqned  2421  neirr  2423  eqneqall  2424  dcne  2425  nonconne  2426  neeq1  2427  neeq2  2428  neneqd  2435  necon3abii  2450  necon3bii  2452  necon3abid  2453  necon3bid  2455  necon3ad  2456  necon3bd  2457  necon3d  2458  necon3ai  2463  necon3bi  2464  necon1aidc  2465  necon1bidc  2466  necon1idc  2467  necon2ai  2468  necon2ad  2471  necon2bd  2472  necon2d  2473  necon1abiidc  2474  necon1bbiidc  2475  necon1abiddc  2476  necon1bbiddc  2477  necon4aidc  2482  necon4idc  2483  necon4addc  2484  necon4bddc  2485  necon4ddc  2486  necon4abiddc  2487  necon4biddc  2489  necon1addc  2490  necon1bddc  2491  necon1ddc  2492  neanior  2501  ne3anior  2502  nemtbir  2503  nfne  2507  nfned  2508  sbcne12g  3159  dfdif3  3333  ifnefalse  3637  opthpr  3881  prneimg  3883  exmid1dc  4318  exmid1stab  4326  onsucelsucexmid  4657  nnsuc  4743  ftpg  5873  fvdifsuppst  6457  suppssrst  6474  suppssrgst  6475  fiintim  7204  updjudhf  7383  netap  7584  elni2  7645  indpi  7673  nngt1ne1  9292  zapne  9672  prime  9698  elnn1uz2  9960  xrnemnf  10132  xrnepnf  10133  xaddcom  10216  xnegdi  10223  xpncan  10226  xleadd1a  10228  xsubge0  10236  flqeqceilz  10707  ndvdssub  12644  gcdsupex  12681  gcdsupcl  12682  gcdeq0  12701  gcd0id  12703  gcdmultiplez  12745  dvdssq  12755  algcvgblem  12774  lcmdvds  12804  lcmid  12805  mulgcddvds  12819  cncongr2  12829  isprm3  12843  isprm4  12844  sqrt2irr  12887  pcxcl  13037  isnzr2  14432  lgscllem  16009  umgr2edg1  16333  eupth2lem1  16582  eupth2lem3lem4fi  16597  bdne  16762  apdifflemr  16970