Definition df-ne 2328

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

This definition is referenced by:  neii  2329  neir  2330  nner  2331  nnedc  2332  dcned  2333  neqned  2334  neirr  2336  eqneqall  2337  dcne  2338  nonconne  2339  neeq1  2340  neeq2  2341  neneqd  2348  necon3abii  2363  necon3bii  2365  necon3abid  2366  necon3bid  2368  necon3ad  2369  necon3bd  2370  necon3d  2371  necon3ai  2376  necon3bi  2377  necon1aidc  2378  necon1bidc  2379  necon1idc  2380  necon2ai  2381  necon2ad  2384  necon2bd  2385  necon2d  2386  necon1abiidc  2387  necon1bbiidc  2388  necon1abiddc  2389  necon1bbiddc  2390  necon4aidc  2395  necon4idc  2396  necon4addc  2397  necon4bddc  2398  necon4ddc  2399  necon4abiddc  2400  necon4biddc  2402  necon1addc  2403  necon1bddc  2404  necon1ddc  2405  neanior  2414  ne3anior  2415  nemtbir  2416  nfne  2420  nfned  2421  sbcne12g  3049  dfdif3  3217  ifnefalse  3516  opthpr  3735  prneimg  3737  exmid1dc  4161  onsucelsucexmid  4488  nnsuc  4574  ftpg  5650  fiintim  6870  updjudhf  7017  elni2  7228  indpi  7256  nngt1ne1  8862  zapne  9232  prime  9257  elnn1uz2  9511  xrnemnf  9677  xrnepnf  9678  xaddcom  9758  xnegdi  9765  xpncan  9768  xleadd1a  9770  xsubge0  9778  flqeqceilz  10210  ndvdssub  11813  gcdsupex  11832  gcdsupcl  11833  gcdeq0  11852  gcd0id  11854  gcdmultiplez  11896  dvdssq  11906  algcvgblem  11917  lcmdvds  11947  lcmid  11948  mulgcddvds  11962  cncongr2  11972  isprm3  11986  isprm4  11987  sqrt2irr  12027  bdne  13399  exmid1stab  13543  apdifflemr  13589