Definition df-ne 2365

Description: Define inequality. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-ne	⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)

Detailed syntax breakdown of Definition df-ne

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wne 2364	. 2 wff 𝐴 ≠ 𝐵
4	1, 2	wceq 1364	. . 3 wff 𝐴 = 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 = 𝐵
6	3, 5	wb 105	1 wff (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)

This definition is referenced by:  neii  2366  neir  2367  nner  2368  nnedc  2369  dcned  2370  neqned  2371  neirr  2373  eqneqall  2374  dcne  2375  nonconne  2376  neeq1  2377  neeq2  2378  neneqd  2385  necon3abii  2400  necon3bii  2402  necon3abid  2403  necon3bid  2405  necon3ad  2406  necon3bd  2407  necon3d  2408  necon3ai  2413  necon3bi  2414  necon1aidc  2415  necon1bidc  2416  necon1idc  2417  necon2ai  2418  necon2ad  2421  necon2bd  2422  necon2d  2423  necon1abiidc  2424  necon1bbiidc  2425  necon1abiddc  2426  necon1bbiddc  2427  necon4aidc  2432  necon4idc  2433  necon4addc  2434  necon4bddc  2435  necon4ddc  2436  necon4abiddc  2437  necon4biddc  2439  necon1addc  2440  necon1bddc  2441  necon1ddc  2442  neanior  2451  ne3anior  2452  nemtbir  2453  nfne  2457  nfned  2458  sbcne12g  3099  dfdif3  3270  ifnefalse  3569  opthpr  3799  prneimg  3801  exmid1dc  4230  exmid1stab  4238  onsucelsucexmid  4563  nnsuc  4649  ftpg  5743  fiintim  6987  updjudhf  7140  netap  7316  elni2  7376  indpi  7404  nngt1ne1  9019  zapne  9394  prime  9419  elnn1uz2  9675  xrnemnf  9846  xrnepnf  9847  xaddcom  9930  xnegdi  9937  xpncan  9940  xleadd1a  9942  xsubge0  9950  flqeqceilz  10392  ndvdssub  12074  gcdsupex  12097  gcdsupcl  12098  gcdeq0  12117  gcd0id  12119  gcdmultiplez  12161  dvdssq  12171  algcvgblem  12190  lcmdvds  12220  lcmid  12221  mulgcddvds  12235  cncongr2  12245  isprm3  12259  isprm4  12260  sqrt2irr  12303  pcxcl  12452  isnzr2  13683  lgscllem  15164  bdne  15415  apdifflemr  15607