Definition df-ne 2368

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 2367	. 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  2369  neir  2370  nner  2371  nnedc  2372  dcned  2373  neqned  2374  neirr  2376  eqneqall  2377  dcne  2378  nonconne  2379  neeq1  2380  neeq2  2381  neneqd  2388  necon3abii  2403  necon3bii  2405  necon3abid  2406  necon3bid  2408  necon3ad  2409  necon3bd  2410  necon3d  2411  necon3ai  2416  necon3bi  2417  necon1aidc  2418  necon1bidc  2419  necon1idc  2420  necon2ai  2421  necon2ad  2424  necon2bd  2425  necon2d  2426  necon1abiidc  2427  necon1bbiidc  2428  necon1abiddc  2429  necon1bbiddc  2430  necon4aidc  2435  necon4idc  2436  necon4addc  2437  necon4bddc  2438  necon4ddc  2439  necon4abiddc  2440  necon4biddc  2442  necon1addc  2443  necon1bddc  2444  necon1ddc  2445  neanior  2454  ne3anior  2455  nemtbir  2456  nfne  2460  nfned  2461  sbcne12g  3102  dfdif3  3274  ifnefalse  3573  opthpr  3803  prneimg  3805  exmid1dc  4234  exmid1stab  4242  onsucelsucexmid  4567  nnsuc  4653  ftpg  5749  fiintim  7001  updjudhf  7154  netap  7339  elni2  7400  indpi  7428  nngt1ne1  9044  zapne  9419  prime  9444  elnn1uz2  9700  xrnemnf  9871  xrnepnf  9872  xaddcom  9955  xnegdi  9962  xpncan  9965  xleadd1a  9967  xsubge0  9975  flqeqceilz  10429  ndvdssub  12114  gcdsupex  12151  gcdsupcl  12152  gcdeq0  12171  gcd0id  12173  gcdmultiplez  12215  dvdssq  12225  algcvgblem  12244  lcmdvds  12274  lcmid  12275  mulgcddvds  12289  cncongr2  12299  isprm3  12313  isprm4  12314  sqrt2irr  12357  pcxcl  12507  isnzr2  13818  lgscllem  15356  bdne  15607  apdifflemr  15804