Definition df-ne 2246

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

This definition is referenced by:  neii  2247  neir  2248  nner  2249  nnedc  2250  dcned  2251  neqned  2252  neirr  2254  eqneqall  2255  dcne  2256  nonconne  2257  neeq1  2258  neeq2  2259  neneqd  2266  necon3abii  2281  necon3bii  2283  necon3abid  2284  necon3bid  2286  necon3ad  2287  necon3bd  2288  necon3d  2289  necon3ai  2294  necon3bi  2295  necon1aidc  2296  necon1bidc  2297  necon1idc  2298  necon2ai  2299  necon2ad  2302  necon2bd  2303  necon2d  2304  necon1abiidc  2305  necon1bbiidc  2306  necon1abiddc  2307  necon1bbiddc  2308  necon4aidc  2313  necon4idc  2314  necon4addc  2315  necon4bddc  2316  necon4ddc  2317  necon4abiddc  2318  necon4biddc  2320  necon1addc  2321  necon1bddc  2322  necon1ddc  2323  neanior  2332  ne3anior  2333  nemtbir  2334  nfne  2337  nfned  2338  sbcne12g  2924  ifnefalse  3362  opthpr  3564  prneimg  3566  onsucelsucexmid  4273  nnsuc  4356  ftpg  5368  elni2  6504  indpi  6532  nngt1ne1  8073  zapne  8422  prime  8446  elnn1uz2  8694  xrnemnf  8853  xrnepnf  8854  flqeqceilz  9320  ndvdssub  10330  gcdsupex  10349  gcdsupcl  10350  gcdeq0  10368  gcd0id  10370  gcdmultiplez  10410  dvdssq  10420  algcvgblem  10431  lcmdvds  10461  lcmid  10462  mulgcddvds  10476  cncongr2  10486  isprm3  10500  isprm4  10501  sqrt2irr  10541  bdne  10644