Definition df-ne 2401

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

This definition is referenced by:  neii  2402  neir  2403  nner  2404  nnedc  2405  dcned  2406  neqned  2407  neirr  2409  eqneqall  2410  dcne  2411  nonconne  2412  neeq1  2413  neeq2  2414  neneqd  2421  necon3abii  2436  necon3bii  2438  necon3abid  2439  necon3bid  2441  necon3ad  2442  necon3bd  2443  necon3d  2444  necon3ai  2449  necon3bi  2450  necon1aidc  2451  necon1bidc  2452  necon1idc  2453  necon2ai  2454  necon2ad  2457  necon2bd  2458  necon2d  2459  necon1abiidc  2460  necon1bbiidc  2461  necon1abiddc  2462  necon1bbiddc  2463  necon4aidc  2468  necon4idc  2469  necon4addc  2470  necon4bddc  2471  necon4ddc  2472  necon4abiddc  2473  necon4biddc  2475  necon1addc  2476  necon1bddc  2477  necon1ddc  2478  neanior  2487  ne3anior  2488  nemtbir  2489  nfne  2493  nfned  2494  sbcne12g  3142  dfdif3  3314  ifnefalse  3613  opthpr  3850  prneimg  3852  exmid1dc  4284  exmid1stab  4292  onsucelsucexmid  4622  nnsuc  4708  ftpg  5827  fiintim  7104  updjudhf  7257  netap  7451  elni2  7512  indpi  7540  nngt1ne1  9156  zapne  9532  prime  9557  elnn1uz2  9814  xrnemnf  9985  xrnepnf  9986  xaddcom  10069  xnegdi  10076  xpncan  10079  xleadd1a  10081  xsubge0  10089  flqeqceilz  10552  ndvdssub  12456  gcdsupex  12493  gcdsupcl  12494  gcdeq0  12513  gcd0id  12515  gcdmultiplez  12557  dvdssq  12567  algcvgblem  12586  lcmdvds  12616  lcmid  12617  mulgcddvds  12631  cncongr2  12641  isprm3  12655  isprm4  12656  sqrt2irr  12699  pcxcl  12849  isnzr2  14163  lgscllem  15701  umgr2edg1  16022  bdne  16271  apdifflemr  16475