Definition df-ne 2268

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 2267	. 2 wff A =/= B
4	1, 2	wceq 1299	. . 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  2269  neir  2270  nner  2271  nnedc  2272  dcned  2273  neqned  2274  neirr  2276  eqneqall  2277  dcne  2278  nonconne  2279  neeq1  2280  neeq2  2281  neneqd  2288  necon3abii  2303  necon3bii  2305  necon3abid  2306  necon3bid  2308  necon3ad  2309  necon3bd  2310  necon3d  2311  necon3ai  2316  necon3bi  2317  necon1aidc  2318  necon1bidc  2319  necon1idc  2320  necon2ai  2321  necon2ad  2324  necon2bd  2325  necon2d  2326  necon1abiidc  2327  necon1bbiidc  2328  necon1abiddc  2329  necon1bbiddc  2330  necon4aidc  2335  necon4idc  2336  necon4addc  2337  necon4bddc  2338  necon4ddc  2339  necon4abiddc  2340  necon4biddc  2342  necon1addc  2343  necon1bddc  2344  necon1ddc  2345  neanior  2354  ne3anior  2355  nemtbir  2356  nfne  2360  nfned  2361  sbcne12g  2971  dfdif3  3133  ifnefalse  3432  opthpr  3646  prneimg  3648  onsucelsucexmid  4383  nnsuc  4467  ftpg  5536  fiintim  6746  updjudhf  6879  elni2  7023  indpi  7051  cnstab  8272  nngt1ne1  8613  zapne  8977  prime  9002  elnn1uz2  9251  xrnemnf  9405  xrnepnf  9406  xaddcom  9485  xnegdi  9492  xpncan  9495  xleadd1a  9497  xsubge0  9505  flqeqceilz  9932  ndvdssub  11422  gcdsupex  11441  gcdsupcl  11442  gcdeq0  11460  gcd0id  11462  gcdmultiplez  11502  dvdssq  11512  algcvgblem  11523  lcmdvds  11553  lcmid  11554  mulgcddvds  11568  cncongr2  11578  isprm3  11592  isprm4  11593  sqrt2irr  11633  bdne  12632