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  3158  dfdif3  3331  ifnefalse  3635  opthpr  3878  prneimg  3880  exmid1dc  4315  exmid1stab  4323  onsucelsucexmid  4654  nnsuc  4740  ftpg  5870  fvdifsuppst  6446  suppssrst  6463  suppssrgst  6464  fiintim  7193  updjudhf  7372  netap  7570  elni2  7631  indpi  7659  nngt1ne1  9274  zapne  9654  prime  9680  elnn1uz2  9942  xrnemnf  10113  xrnepnf  10114  xaddcom  10197  xnegdi  10204  xpncan  10207  xleadd1a  10209  xsubge0  10217  flqeqceilz  10684  ndvdssub  12620  gcdsupex  12657  gcdsupcl  12658  gcdeq0  12677  gcd0id  12679  gcdmultiplez  12721  dvdssq  12731  algcvgblem  12750  lcmdvds  12780  lcmid  12781  mulgcddvds  12795  cncongr2  12805  isprm3  12819  isprm4  12820  sqrt2irr  12863  pcxcl  13013  isnzr2  14346  lgscllem  15897  umgr2edg1  16221  eupth2lem1  16470  eupth2lem3lem4fi  16485  bdne  16640  apdifflemr  16848