Definition df-ne 2379

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 2378	. 2 wff A =/= B
4	1, 2	wceq 1373	. . 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  2380  neir  2381  nner  2382  nnedc  2383  dcned  2384  neqned  2385  neirr  2387  eqneqall  2388  dcne  2389  nonconne  2390  neeq1  2391  neeq2  2392  neneqd  2399  necon3abii  2414  necon3bii  2416  necon3abid  2417  necon3bid  2419  necon3ad  2420  necon3bd  2421  necon3d  2422  necon3ai  2427  necon3bi  2428  necon1aidc  2429  necon1bidc  2430  necon1idc  2431  necon2ai  2432  necon2ad  2435  necon2bd  2436  necon2d  2437  necon1abiidc  2438  necon1bbiidc  2439  necon1abiddc  2440  necon1bbiddc  2441  necon4aidc  2446  necon4idc  2447  necon4addc  2448  necon4bddc  2449  necon4ddc  2450  necon4abiddc  2451  necon4biddc  2453  necon1addc  2454  necon1bddc  2455  necon1ddc  2456  neanior  2465  ne3anior  2466  nemtbir  2467  nfne  2471  nfned  2472  sbcne12g  3119  dfdif3  3291  ifnefalse  3590  opthpr  3826  prneimg  3828  exmid1dc  4260  exmid1stab  4268  onsucelsucexmid  4596  nnsuc  4682  ftpg  5791  fiintim  7054  updjudhf  7207  netap  7401  elni2  7462  indpi  7490  nngt1ne1  9106  zapne  9482  prime  9507  elnn1uz2  9763  xrnemnf  9934  xrnepnf  9935  xaddcom  10018  xnegdi  10025  xpncan  10028  xleadd1a  10030  xsubge0  10038  flqeqceilz  10500  ndvdssub  12356  gcdsupex  12393  gcdsupcl  12394  gcdeq0  12413  gcd0id  12415  gcdmultiplez  12457  dvdssq  12467  algcvgblem  12486  lcmdvds  12516  lcmid  12517  mulgcddvds  12531  cncongr2  12541  isprm3  12555  isprm4  12556  sqrt2irr  12599  pcxcl  12749  isnzr2  14061  lgscllem  15599  bdne  15988  apdifflemr  16188