Definition df-ne 2341

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 2340	. 2 wff A =/= B
4	1, 2	wceq 1348	. . 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  2342  neir  2343  nner  2344  nnedc  2345  dcned  2346  neqned  2347  neirr  2349  eqneqall  2350  dcne  2351  nonconne  2352  neeq1  2353  neeq2  2354  neneqd  2361  necon3abii  2376  necon3bii  2378  necon3abid  2379  necon3bid  2381  necon3ad  2382  necon3bd  2383  necon3d  2384  necon3ai  2389  necon3bi  2390  necon1aidc  2391  necon1bidc  2392  necon1idc  2393  necon2ai  2394  necon2ad  2397  necon2bd  2398  necon2d  2399  necon1abiidc  2400  necon1bbiidc  2401  necon1abiddc  2402  necon1bbiddc  2403  necon4aidc  2408  necon4idc  2409  necon4addc  2410  necon4bddc  2411  necon4ddc  2412  necon4abiddc  2413  necon4biddc  2415  necon1addc  2416  necon1bddc  2417  necon1ddc  2418  neanior  2427  ne3anior  2428  nemtbir  2429  nfne  2433  nfned  2434  sbcne12g  3067  dfdif3  3237  ifnefalse  3536  opthpr  3757  prneimg  3759  exmid1dc  4184  onsucelsucexmid  4512  nnsuc  4598  ftpg  5677  fiintim  6902  updjudhf  7052  elni2  7263  indpi  7291  nngt1ne1  8900  zapne  9273  prime  9298  elnn1uz2  9553  xrnemnf  9721  xrnepnf  9722  xaddcom  9805  xnegdi  9812  xpncan  9815  xleadd1a  9817  xsubge0  9825  flqeqceilz  10261  ndvdssub  11876  gcdsupex  11899  gcdsupcl  11900  gcdeq0  11919  gcd0id  11921  gcdmultiplez  11963  dvdssq  11973  algcvgblem  11990  lcmdvds  12020  lcmid  12021  mulgcddvds  12035  cncongr2  12045  isprm3  12059  isprm4  12060  sqrt2irr  12103  pcxcl  12252  lgscllem  13661  bdne  13848  exmid1stab  13993  apdifflemr  14039