Definition df-ne 2413

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 2412	. 2 wff A =/= B
4	1, 2	wceq 1398	. . 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  2414  neir  2415  nner  2416  nnedc  2417  dcned  2418  neqned  2419  neirr  2421  eqneqall  2422  dcne  2423  nonconne  2424  neeq1  2425  neeq2  2426  neneqd  2433  necon3abii  2448  necon3bii  2450  necon3abid  2451  necon3bid  2453  necon3ad  2454  necon3bd  2455  necon3d  2456  necon3ai  2461  necon3bi  2462  necon1aidc  2463  necon1bidc  2464  necon1idc  2465  necon2ai  2466  necon2ad  2469  necon2bd  2470  necon2d  2471  necon1abiidc  2472  necon1bbiidc  2473  necon1abiddc  2474  necon1bbiddc  2475  necon4aidc  2480  necon4idc  2481  necon4addc  2482  necon4bddc  2483  necon4ddc  2484  necon4abiddc  2485  necon4biddc  2487  necon1addc  2488  necon1bddc  2489  necon1ddc  2490  neanior  2499  ne3anior  2500  nemtbir  2501  nfne  2505  nfned  2506  sbcne12g  3155  dfdif3  3328  ifnefalse  3632  opthpr  3875  prneimg  3877  exmid1dc  4312  exmid1stab  4320  onsucelsucexmid  4651  nnsuc  4737  ftpg  5867  fvdifsuppst  6443  suppssrst  6460  suppssrgst  6461  fiintim  7190  updjudhf  7369  netap  7564  elni2  7625  indpi  7653  nngt1ne1  9268  zapne  9648  prime  9673  elnn1uz2  9935  xrnemnf  10106  xrnepnf  10107  xaddcom  10190  xnegdi  10197  xpncan  10200  xleadd1a  10202  xsubge0  10210  flqeqceilz  10676  ndvdssub  12609  gcdsupex  12646  gcdsupcl  12647  gcdeq0  12666  gcd0id  12668  gcdmultiplez  12710  dvdssq  12720  algcvgblem  12739  lcmdvds  12769  lcmid  12770  mulgcddvds  12784  cncongr2  12794  isprm3  12808  isprm4  12809  sqrt2irr  12852  pcxcl  13002  isnzr2  14318  lgscllem  15867  umgr2edg1  16191  eupth2lem1  16440  eupth2lem3lem4fi  16455  bdne  16610  apdifflemr  16818