Definition df-ne 2348

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 2347	. 2 wff A =/= B
4	1, 2	wceq 1353	. . 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  2349  neir  2350  nner  2351  nnedc  2352  dcned  2353  neqned  2354  neirr  2356  eqneqall  2357  dcne  2358  nonconne  2359  neeq1  2360  neeq2  2361  neneqd  2368  necon3abii  2383  necon3bii  2385  necon3abid  2386  necon3bid  2388  necon3ad  2389  necon3bd  2390  necon3d  2391  necon3ai  2396  necon3bi  2397  necon1aidc  2398  necon1bidc  2399  necon1idc  2400  necon2ai  2401  necon2ad  2404  necon2bd  2405  necon2d  2406  necon1abiidc  2407  necon1bbiidc  2408  necon1abiddc  2409  necon1bbiddc  2410  necon4aidc  2415  necon4idc  2416  necon4addc  2417  necon4bddc  2418  necon4ddc  2419  necon4abiddc  2420  necon4biddc  2422  necon1addc  2423  necon1bddc  2424  necon1ddc  2425  neanior  2434  ne3anior  2435  nemtbir  2436  nfne  2440  nfned  2441  sbcne12g  3076  dfdif3  3246  ifnefalse  3546  opthpr  3773  prneimg  3775  exmid1dc  4201  exmid1stab  4209  onsucelsucexmid  4530  nnsuc  4616  ftpg  5701  fiintim  6928  updjudhf  7078  netap  7253  elni2  7313  indpi  7341  nngt1ne1  8954  zapne  9327  prime  9352  elnn1uz2  9607  xrnemnf  9777  xrnepnf  9778  xaddcom  9861  xnegdi  9868  xpncan  9871  xleadd1a  9873  xsubge0  9881  flqeqceilz  10318  ndvdssub  11935  gcdsupex  11958  gcdsupcl  11959  gcdeq0  11978  gcd0id  11980  gcdmultiplez  12022  dvdssq  12032  algcvgblem  12049  lcmdvds  12079  lcmid  12080  mulgcddvds  12094  cncongr2  12104  isprm3  12118  isprm4  12119  sqrt2irr  12162  pcxcl  12311  lgscllem  14411  bdne  14608  apdifflemr  14798