Definition df-ne 2415

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

This definition is referenced by:  neii  2416  neir  2417  nner  2418  nnedc  2419  dcned  2420  neqned  2421  neirr  2423  eqneqall  2424  dcne  2425  nonconne  2426  neeq1  2427  neeq2  2428  neneqd  2435  necon3abii  2450  necon3bii  2452  necon3abid  2453  necon3bid  2455  necon3ad  2456  necon3bd  2457  necon3d  2458  necon3ai  2463  necon3bi  2464  necon1aidc  2465  necon1bidc  2466  necon1idc  2467  necon2ai  2468  necon2ad  2471  necon2bd  2472  necon2d  2473  necon1abiidc  2474  necon1bbiidc  2475  necon1abiddc  2476  necon1bbiddc  2477  necon4aidc  2482  necon4idc  2483  necon4addc  2484  necon4bddc  2485  necon4ddc  2486  necon4abiddc  2487  necon4biddc  2489  necon1addc  2490  necon1bddc  2491  necon1ddc  2492  neanior  2501  ne3anior  2502  nemtbir  2503  nfne  2507  nfned  2508  sbcne12g  3159  dfdif3  3333  ifnefalse  3637  opthpr  3881  prneimg  3883  exmid1dc  4318  exmid1stab  4326  onsucelsucexmid  4657  nnsuc  4743  ftpg  5873  fvdifsuppst  6457  suppssrst  6474  suppssrgst  6475  fiintim  7204  updjudhf  7383  netap  7584  elni2  7645  indpi  7673  nngt1ne1  9289  zapne  9669  prime  9695  elnn1uz2  9957  xrnemnf  10129  xrnepnf  10130  xaddcom  10213  xnegdi  10220  xpncan  10223  xleadd1a  10225  xsubge0  10233  flqeqceilz  10704  ndvdssub  12641  gcdsupex  12678  gcdsupcl  12679  gcdeq0  12698  gcd0id  12700  gcdmultiplez  12742  dvdssq  12752  algcvgblem  12771  lcmdvds  12801  lcmid  12802  mulgcddvds  12816  cncongr2  12826  isprm3  12840  isprm4  12841  sqrt2irr  12884  pcxcl  13034  isnzr2  14429  lgscllem  16006  umgr2edg1  16330  eupth2lem1  16579  eupth2lem3lem4fi  16594  bdne  16749  apdifflemr  16957