Definition df-ne 2421

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

This definition is used by:  neii  2422  neir  2423  nner  2424  nnedc  2425  dcned  2426  neqned  2427  neirr  2429  eqneqall  2430  dcne  2431  nonconne  2432  neeq1  2433  neeq2  2434  neneqd  2441  necon3abii  2456  necon3bii  2458  necon3abid  2459  necon3bid  2461  necon3ad  2462  necon3bd  2463  necon3d  2464  necon3ai  2469  necon3bi  2470  necon1aidc  2471  necon1bidc  2472  necon1idc  2473  necon2ai  2474  necon2ad  2477  necon2bd  2478  necon2d  2479  necon1abiidc  2480  necon1bbiidc  2481  necon1abiddc  2482  necon1bbiddc  2483  necon4aidc  2488  necon4idc  2489  necon4addc  2490  necon4bddc  2491  necon4ddc  2492  necon4abiddc  2493  necon4biddc  2495  necon1addc  2496  necon1bddc  2497  necon1ddc  2498  neanior  2507  ne3anior  2508  nemtbir  2509  nfne  2513  nfned  2514  sbcne12g  3165  dfdif3  3339  ifnefalse  3651  opthpr  3897  prneimg  3899  exmid1dc  4339  exmid1stab  4347  onsucelsucexmid  4679  nnsuc  4765  ftpg  5902  fvdifsuppst  6488  suppssrst  6505  suppssrgst  6506  fiintim  7244  updjudhf  7425  netap  7626  elni2  7687  indpi  7715  nngt1ne1  9348  zapne  9728  prime  9755  elnn1uz2  10022  xrnemnf  10195  xrnepnf  10196  xaddcom  10279  xnegdi  10286  xpncan  10289  xleadd1a  10291  xsubge0  10299  flqeqceilz  10775  ndvdssub  12721  gcdsupex  12758  gcdsupcl  12759  gcdeq0  12778  gcd0id  12780  gcdmultiplez  12822  dvdssq  12832  algcvgblem  12851  lcmdvds  12881  lcmid  12882  mulgcddvds  12896  cncongr2  12906  isprm3  12920  isprm4  12921  sqrt2irr  12965  pcxcl  13118  isnzr2  14599  ppiqeq0  16297  lgscllem  16348  umgr2edg1  16672  eupth2lem1  16921  eupth2lem3lem4fi  16936  bdne  17101  apdifflemr  17320