Definition df-ne 2348

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

This definition is referenced by:  neii  2349  neir  2350  nner  2351  nnedc  2352  dcned  2353  neqned  2354  neirr  2356  eqneqall  2357  dcne  2358  nonconne  2359  neeq1  2360  neeq2  2361  neneqd  2368  necon3abii  2383  necon3bii  2385  necon3abid  2386  necon3bid  2388  necon3ad  2389  necon3bd  2390  necon3d  2391  necon3ai  2396  necon3bi  2397  necon1aidc  2398  necon1bidc  2399  necon1idc  2400  necon2ai  2401  necon2ad  2404  necon2bd  2405  necon2d  2406  necon1abiidc  2407  necon1bbiidc  2408  necon1abiddc  2409  necon1bbiddc  2410  necon4aidc  2415  necon4idc  2416  necon4addc  2417  necon4bddc  2418  necon4ddc  2419  necon4abiddc  2420  necon4biddc  2422  necon1addc  2423  necon1bddc  2424  necon1ddc  2425  neanior  2434  ne3anior  2435  nemtbir  2436  nfne  2440  nfned  2441  sbcne12g  3075  dfdif3  3245  ifnefalse  3545  opthpr  3772  prneimg  3774  exmid1dc  4200  exmid1stab  4208  onsucelsucexmid  4529  nnsuc  4615  ftpg  5700  fiintim  6927  updjudhf  7077  netap  7252  elni2  7312  indpi  7340  nngt1ne1  8953  zapne  9326  prime  9351  elnn1uz2  9606  xrnemnf  9776  xrnepnf  9777  xaddcom  9860  xnegdi  9867  xpncan  9870  xleadd1a  9872  xsubge0  9880  flqeqceilz  10317  ndvdssub  11934  gcdsupex  11957  gcdsupcl  11958  gcdeq0  11977  gcd0id  11979  gcdmultiplez  12021  dvdssq  12031  algcvgblem  12048  lcmdvds  12078  lcmid  12079  mulgcddvds  12093  cncongr2  12103  isprm3  12117  isprm4  12118  sqrt2irr  12161  pcxcl  12310  lgscllem  14378  bdne  14575  apdifflemr  14765