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  3098  dfdif3  3269  ifnefalse  3568  opthpr  3798  prneimg  3800  exmid1dc  4229  exmid1stab  4237  onsucelsucexmid  4562  nnsuc  4648  ftpg  5742  fiintim  6985  updjudhf  7138  netap  7314  elni2  7374  indpi  7402  nngt1ne1  9017  zapne  9391  prime  9416  elnn1uz2  9672  xrnemnf  9843  xrnepnf  9844  xaddcom  9927  xnegdi  9934  xpncan  9937  xleadd1a  9939  xsubge0  9947  flqeqceilz  10389  ndvdssub  12071  gcdsupex  12094  gcdsupcl  12095  gcdeq0  12114  gcd0id  12116  gcdmultiplez  12158  dvdssq  12168  algcvgblem  12187  lcmdvds  12217  lcmid  12218  mulgcddvds  12232  cncongr2  12242  isprm3  12256  isprm4  12257  sqrt2irr  12300  pcxcl  12449  isnzr2  13680  lgscllem  15123  bdne  15345  apdifflemr  15537