Definition df-ne 2310

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 2309	. 2 wff A =/= B
4	1, 2	wceq 1332	. . 3 wff A = B
5	4	wn 3	. 2 wff -. A = B
6	3, 5	wb 104	1 wff ( A =/= B <-> -. A = B )

This definition is referenced by:  neii  2311  neir  2312  nner  2313  nnedc  2314  dcned  2315  neqned  2316  neirr  2318  eqneqall  2319  dcne  2320  nonconne  2321  neeq1  2322  neeq2  2323  neneqd  2330  necon3abii  2345  necon3bii  2347  necon3abid  2348  necon3bid  2350  necon3ad  2351  necon3bd  2352  necon3d  2353  necon3ai  2358  necon3bi  2359  necon1aidc  2360  necon1bidc  2361  necon1idc  2362  necon2ai  2363  necon2ad  2366  necon2bd  2367  necon2d  2368  necon1abiidc  2369  necon1bbiidc  2370  necon1abiddc  2371  necon1bbiddc  2372  necon4aidc  2377  necon4idc  2378  necon4addc  2379  necon4bddc  2380  necon4ddc  2381  necon4abiddc  2382  necon4biddc  2384  necon1addc  2385  necon1bddc  2386  necon1ddc  2387  neanior  2396  ne3anior  2397  nemtbir  2398  nfne  2402  nfned  2403  sbcne12g  3025  dfdif3  3191  ifnefalse  3490  opthpr  3707  prneimg  3709  exmid1dc  4131  onsucelsucexmid  4453  nnsuc  4537  ftpg  5612  fiintim  6825  updjudhf  6972  elni2  7146  indpi  7174  cnstab  8431  nngt1ne1  8779  zapne  9149  prime  9174  elnn1uz2  9428  xrnemnf  9594  xrnepnf  9595  xaddcom  9674  xnegdi  9681  xpncan  9684  xleadd1a  9686  xsubge0  9694  flqeqceilz  10122  ndvdssub  11663  gcdsupex  11682  gcdsupcl  11683  gcdeq0  11701  gcd0id  11703  gcdmultiplez  11745  dvdssq  11755  algcvgblem  11766  lcmdvds  11796  lcmid  11797  mulgcddvds  11811  cncongr2  11821  isprm3  11835  isprm4  11836  sqrt2irr  11876  bdne  13222  exmid1stab  13368  apdifflemr  13415