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  3849  prneimg  3851  exmid1dc  4283  exmid1stab  4291  onsucelsucexmid  4621  nnsuc  4707  ftpg  5822  fiintim  7089  updjudhf  7242  netap  7436  elni2  7497  indpi  7525  nngt1ne1  9141  zapne  9517  prime  9542  elnn1uz2  9798  xrnemnf  9969  xrnepnf  9970  xaddcom  10053  xnegdi  10060  xpncan  10063  xleadd1a  10065  xsubge0  10073  flqeqceilz  10535  ndvdssub  12436  gcdsupex  12473  gcdsupcl  12474  gcdeq0  12493  gcd0id  12495  gcdmultiplez  12537  dvdssq  12547  algcvgblem  12566  lcmdvds  12596  lcmid  12597  mulgcddvds  12611  cncongr2  12621  isprm3  12635  isprm4  12636  sqrt2irr  12679  pcxcl  12829  isnzr2  14142  lgscllem  15680  umgr2edg1  16001  bdne  16174  apdifflemr  16374