Definition df-ne 2368

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 2367	. 2 wff A =/= B
4	1, 2	wceq 1364	. . 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  2369  neir  2370  nner  2371  nnedc  2372  dcned  2373  neqned  2374  neirr  2376  eqneqall  2377  dcne  2378  nonconne  2379  neeq1  2380  neeq2  2381  neneqd  2388  necon3abii  2403  necon3bii  2405  necon3abid  2406  necon3bid  2408  necon3ad  2409  necon3bd  2410  necon3d  2411  necon3ai  2416  necon3bi  2417  necon1aidc  2418  necon1bidc  2419  necon1idc  2420  necon2ai  2421  necon2ad  2424  necon2bd  2425  necon2d  2426  necon1abiidc  2427  necon1bbiidc  2428  necon1abiddc  2429  necon1bbiddc  2430  necon4aidc  2435  necon4idc  2436  necon4addc  2437  necon4bddc  2438  necon4ddc  2439  necon4abiddc  2440  necon4biddc  2442  necon1addc  2443  necon1bddc  2444  necon1ddc  2445  neanior  2454  ne3anior  2455  nemtbir  2456  nfne  2460  nfned  2461  sbcne12g  3102  dfdif3  3273  ifnefalse  3572  opthpr  3802  prneimg  3804  exmid1dc  4233  exmid1stab  4241  onsucelsucexmid  4566  nnsuc  4652  ftpg  5746  fiintim  6992  updjudhf  7145  netap  7321  elni2  7381  indpi  7409  nngt1ne1  9025  zapne  9400  prime  9425  elnn1uz2  9681  xrnemnf  9852  xrnepnf  9853  xaddcom  9936  xnegdi  9943  xpncan  9946  xleadd1a  9948  xsubge0  9956  flqeqceilz  10410  ndvdssub  12095  gcdsupex  12124  gcdsupcl  12125  gcdeq0  12144  gcd0id  12146  gcdmultiplez  12188  dvdssq  12198  algcvgblem  12217  lcmdvds  12247  lcmid  12248  mulgcddvds  12262  cncongr2  12272  isprm3  12286  isprm4  12287  sqrt2irr  12330  pcxcl  12480  isnzr2  13740  lgscllem  15248  bdne  15499  apdifflemr  15691