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  3077  dfdif3  3247  ifnefalse  3547  opthpr  3774  prneimg  3776  exmid1dc  4202  exmid1stab  4210  onsucelsucexmid  4531  nnsuc  4617  ftpg  5702  fiintim  6930  updjudhf  7080  netap  7255  elni2  7315  indpi  7343  nngt1ne1  8956  zapne  9329  prime  9354  elnn1uz2  9609  xrnemnf  9779  xrnepnf  9780  xaddcom  9863  xnegdi  9870  xpncan  9873  xleadd1a  9875  xsubge0  9883  flqeqceilz  10320  ndvdssub  11937  gcdsupex  11960  gcdsupcl  11961  gcdeq0  11980  gcd0id  11982  gcdmultiplez  12024  dvdssq  12034  algcvgblem  12051  lcmdvds  12081  lcmid  12082  mulgcddvds  12096  cncongr2  12106  isprm3  12120  isprm4  12121  sqrt2irr  12164  pcxcl  12313  lgscllem  14493  bdne  14690  apdifflemr  14880