Definition df-ne 2336

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 2335	. 2 wff 𝐴 ≠ 𝐵
4	1, 2	wceq 1343	. . 3 wff 𝐴 = 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 = 𝐵
6	3, 5	wb 104	1 wff (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)

This definition is referenced by:  neii  2337  neir  2338  nner  2339  nnedc  2340  dcned  2341  neqned  2342  neirr  2344  eqneqall  2345  dcne  2346  nonconne  2347  neeq1  2348  neeq2  2349  neneqd  2356  necon3abii  2371  necon3bii  2373  necon3abid  2374  necon3bid  2376  necon3ad  2377  necon3bd  2378  necon3d  2379  necon3ai  2384  necon3bi  2385  necon1aidc  2386  necon1bidc  2387  necon1idc  2388  necon2ai  2389  necon2ad  2392  necon2bd  2393  necon2d  2394  necon1abiidc  2395  necon1bbiidc  2396  necon1abiddc  2397  necon1bbiddc  2398  necon4aidc  2403  necon4idc  2404  necon4addc  2405  necon4bddc  2406  necon4ddc  2407  necon4abiddc  2408  necon4biddc  2410  necon1addc  2411  necon1bddc  2412  necon1ddc  2413  neanior  2422  ne3anior  2423  nemtbir  2424  nfne  2428  nfned  2429  sbcne12g  3062  dfdif3  3231  ifnefalse  3530  opthpr  3751  prneimg  3753  exmid1dc  4178  onsucelsucexmid  4506  nnsuc  4592  ftpg  5668  fiintim  6890  updjudhf  7040  elni2  7251  indpi  7279  nngt1ne1  8888  zapne  9261  prime  9286  elnn1uz2  9541  xrnemnf  9709  xrnepnf  9710  xaddcom  9793  xnegdi  9800  xpncan  9803  xleadd1a  9805  xsubge0  9813  flqeqceilz  10249  ndvdssub  11863  gcdsupex  11886  gcdsupcl  11887  gcdeq0  11906  gcd0id  11908  gcdmultiplez  11950  dvdssq  11960  algcvgblem  11977  lcmdvds  12007  lcmid  12008  mulgcddvds  12022  cncongr2  12032  isprm3  12046  isprm4  12047  sqrt2irr  12090  pcxcl  12239  lgscllem  13508  bdne  13695  exmid1stab  13840  apdifflemr  13886