Definition df-ne 2309

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

This definition is referenced by:  neii  2310  neir  2311  nner  2312  nnedc  2313  dcned  2314  neqned  2315  neirr  2317  eqneqall  2318  dcne  2319  nonconne  2320  neeq1  2321  neeq2  2322  neneqd  2329  necon3abii  2344  necon3bii  2346  necon3abid  2347  necon3bid  2349  necon3ad  2350  necon3bd  2351  necon3d  2352  necon3ai  2357  necon3bi  2358  necon1aidc  2359  necon1bidc  2360  necon1idc  2361  necon2ai  2362  necon2ad  2365  necon2bd  2366  necon2d  2367  necon1abiidc  2368  necon1bbiidc  2369  necon1abiddc  2370  necon1bbiddc  2371  necon4aidc  2376  necon4idc  2377  necon4addc  2378  necon4bddc  2379  necon4ddc  2380  necon4abiddc  2381  necon4biddc  2383  necon1addc  2384  necon1bddc  2385  necon1ddc  2386  neanior  2395  ne3anior  2396  nemtbir  2397  nfne  2401  nfned  2402  sbcne12g  3020  dfdif3  3186  ifnefalse  3485  opthpr  3699  prneimg  3701  exmid1dc  4123  onsucelsucexmid  4445  nnsuc  4529  ftpg  5604  fiintim  6817  updjudhf  6964  elni2  7122  indpi  7150  cnstab  8407  nngt1ne1  8755  zapne  9125  prime  9150  elnn1uz2  9401  xrnemnf  9564  xrnepnf  9565  xaddcom  9644  xnegdi  9651  xpncan  9654  xleadd1a  9656  xsubge0  9664  flqeqceilz  10091  ndvdssub  11627  gcdsupex  11646  gcdsupcl  11647  gcdeq0  11665  gcd0id  11667  gcdmultiplez  11709  dvdssq  11719  algcvgblem  11730  lcmdvds  11760  lcmid  11761  mulgcddvds  11775  cncongr2  11785  isprm3  11799  isprm4  11800  sqrt2irr  11840  bdne  13051  exmid1stab  13195