Definition df-ne 2377

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 2376	. 2 wff A =/= B
4	1, 2	wceq 1373	. . 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  2378  neir  2379  nner  2380  nnedc  2381  dcned  2382  neqned  2383  neirr  2385  eqneqall  2386  dcne  2387  nonconne  2388  neeq1  2389  neeq2  2390  neneqd  2397  necon3abii  2412  necon3bii  2414  necon3abid  2415  necon3bid  2417  necon3ad  2418  necon3bd  2419  necon3d  2420  necon3ai  2425  necon3bi  2426  necon1aidc  2427  necon1bidc  2428  necon1idc  2429  necon2ai  2430  necon2ad  2433  necon2bd  2434  necon2d  2435  necon1abiidc  2436  necon1bbiidc  2437  necon1abiddc  2438  necon1bbiddc  2439  necon4aidc  2444  necon4idc  2445  necon4addc  2446  necon4bddc  2447  necon4ddc  2448  necon4abiddc  2449  necon4biddc  2451  necon1addc  2452  necon1bddc  2453  necon1ddc  2454  neanior  2463  ne3anior  2464  nemtbir  2465  nfne  2469  nfned  2470  sbcne12g  3111  dfdif3  3283  ifnefalse  3582  opthpr  3813  prneimg  3815  exmid1dc  4244  exmid1stab  4252  onsucelsucexmid  4578  nnsuc  4664  ftpg  5768  fiintim  7028  updjudhf  7181  netap  7366  elni2  7427  indpi  7455  nngt1ne1  9071  zapne  9447  prime  9472  elnn1uz2  9728  xrnemnf  9899  xrnepnf  9900  xaddcom  9983  xnegdi  9990  xpncan  9993  xleadd1a  9995  xsubge0  10003  flqeqceilz  10463  ndvdssub  12241  gcdsupex  12278  gcdsupcl  12279  gcdeq0  12298  gcd0id  12300  gcdmultiplez  12342  dvdssq  12352  algcvgblem  12371  lcmdvds  12401  lcmid  12402  mulgcddvds  12416  cncongr2  12426  isprm3  12440  isprm4  12441  sqrt2irr  12484  pcxcl  12634  isnzr2  13946  lgscllem  15484  bdne  15789  apdifflemr  15986