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  8952  zapne  9325  prime  9350  elnn1uz2  9605  xrnemnf  9775  xrnepnf  9776  xaddcom  9859  xnegdi  9866  xpncan  9869  xleadd1a  9871  xsubge0  9879  flqeqceilz  10315  ndvdssub  11929  gcdsupex  11952  gcdsupcl  11953  gcdeq0  11972  gcd0id  11974  gcdmultiplez  12016  dvdssq  12026  algcvgblem  12043  lcmdvds  12073  lcmid  12074  mulgcddvds  12088  cncongr2  12098  isprm3  12112  isprm4  12113  sqrt2irr  12156  pcxcl  12305  lgscllem  14301  bdne  14487  apdifflemr  14677