Definition df-ne 2946

Description: Define inequality. (Contributed by NM, 26-May-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 2945	. 2 wff 𝐴 ≠ 𝐵
4	1, 2	wceq 1542	. . 3 wff 𝐴 = 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 = 𝐵
6	3, 5	wb 205	1 wff (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)

This definition is referenced by:  neii  2947  neir  2948  nne  2949  neneqd  2950  neqned  2952  eqneqall  2956  necon2bd  2961  necon1bd  2963  necon3d  2966  necon2d  2968  necon1bi  2974  necon1i  2979  necon3abid  2982  necon1bbid  2985  necon3bid  2990  necon3abii  2992  necon3bii  2998  neor  3038  neanior  3039  neorian  3041  nfne  3047  nfned  3048  nabbi  3049  nelb  3197  nelbOLD  3198  dfpss2  4025  dfdif3  4054  n0f  4282  n0  4286  abn0  4320  2nreu  4381  raaan2  4461  ifnefalse  4477  snnzb  4660  raldifsni  4734  eqsn  4768  n0snor2el  4770  opthpr  4788  opthprneg  4801  unissint  4909  iununi  5033  disji2  5061  opthneg  5399  opab0  5469  xpcan  6077  xpcan2  6078  xpima  6083  unixpid  6185  unizlim  6381  dff14a  7138  orduniorsuc  7669  dflim3  7686  tfindsg  7699  nn0suc  7734  findsg  7738  suppvalbr  7970  frrlem14  8104  wfrlem16OLD  8144  tz7.49  8265  oevn0  8328  fsetexb  8633  php  8972  phpOLD  8985  1sdom  9002  fimaxg  9037  fiint  9067  wemapsolem  9285  card2on  9289  brwdomn0  9304  rankxplim2  9637  rankxplim3  9638  updjudhf  9688  carden2a  9723  dfackm  9921  fin1a2lem12  10166  ac6num  10234  zorn2lem4  10254  zorn2lem7  10257  brdom3  10283  iundom2g  10295  r1tskina  10537  1re  10974  ltlen  11074  uzm1  12613  xrnemnf  12850  xrnepnf  12851  ioo0  13101  ico0  13122  ioc0  13123  icc0  13124  elfznelfzo  13488  elfznelfzob  13489  injresinjlem  13503  fleqceilz  13570  fsuppmapnn0fiubex  13708  sq01  13936  hash1snb  14130  hashgt12el  14133  hashgt12el2  14134  hashfun  14148  hash2prde  14180  hashge2el2dif  14190  fundmge2nop0  14202  repswcshw  14521  cshw1  14531  incexc2  15546  sqrt2irr  15954  divalglem8  16105  ndvdssub  16114  algcvgblem  16278  lcmcllem  16297  lcmfunsnlem2  16341  isprm3  16384  isprm4  16385  2mulprm  16394  ramcl2lem  16706  cshwshashlem1  16793  cshwshash  16802  smndex2dnrinv  18550  sgrp2nmndlem3  18560  sgrp2nmndlem5  18564  symg2bas  18996  odfval  19136  dprdfeq0  19621  isnirred  19938  isirred2  19939  drngmul0or  20008  drngmuleq0  20010  sdrgacs  20065  lvecvs0or  20366  lvecvscan  20369  isnzr2  20530  isdomn2  20566  domnchr  20732  gsummoncoe1  21471  dmatmul  21642  mulmarep1gsum2  21719  mdetunilem8  21764  mp2pm2mplem4  21954  fvmptnn04if  21994  elcls  22220  opnnei  22267  ist0-3  22492  ist1-2  22494  dfconn2  22566  cnconn  22569  pthaus  22785  xkohaus  22800  hausflim  23128  cldsubg  23258  bcth  24489  ioorinv  24736  tdeglem4  25220  tdeglem4OLD  25221  fta1b  25330  plydivex  25453  aalioulem3  25490  dvradcnv  25576  cxpcl  25825  recxpcl  25826  logrec  25909  isosctrlem2  25965  efrlim  26115  muval2  26279  musum  26336  dchrelbas2  26381  dchrelbas4  26387  dchrfi  26399  dchrptlem3  26410  dchrsum2  26412  sumdchr2  26414  lgscllem  26448  2sqb  26576  2sqcoprm  26579  dchrvmasumiflem2  26646  rpvmasum2  26656  padicabv  26774  padicabvf  26775  padicabvcxp  26776  tglowdim1i  26858  tgbtwnconn1  26932  colline  27006  colmid  27045  lmimid  27151  lmiisolem  27153  brbtwn2  27269  colinearalg  27274  axlowdimlem6  27311  axlowdimlem14  27319  axcontlem12  27339  incistruhgr  27445  umgr2edg1  27574  nb3grprlem1  27743  1egrvtxdg0  27874  vtxdginducedm1lem4  27905  wlkdlem4  28048  lfgriswlk  28051  pthdlem2  28130  wwlksnext  28252  clwwlknclwwlkdif  28337  clwlkclwwlklem2a4  28355  clwwisshclwwsn  28374  1wlkdlem4  28498  eupth2lem1  28576  eupth2lem3lem4  28589  frgr3vlem1  28631  frgr3vlem2  28632  3vfriswmgrlem  28635  4cycl2vnunb  28648  frgrncvvdeqlem8  28664  frgrregorufr  28683  frgrreg  28752  frgrregord013  28753  9p10ne21fool  28829  nvmul0or  29006  nmogtmnf  29126  hvmul0or  29381  hvmulcan  29428  hvmulcan2  29429  hiidge0  29454  bcsiALT  29535  shne0i  29804  nonbooli  30007  nmopgtmnf  30224  unopbd  30371  nmcfnlbi  30408  nmopcoi  30451  chirredi  30750  mdsymlem5  30763  sumdmdlem2  30775  nelbOLDOLD  30811  disji2f  30910  aciunf1  30994  fzne1  31103  hashxpe  31121  sitgaddlemb  32309  sgn3da  32502  plymulx  32521  bnj1109  32760  bnj1542  32831  bnj1253  32991  dff15  33050  lfuhgr3  33075  dfacycgr1  33100  subfacp1lem6  33141  cvmsdisj  33226  satffunlem1lem1  33358  satffunlem2lem1  33360  satffun  33365  xpord2pred  33786  xpord2ind  33788  poxp3  33790  frxp3  33791  xpord3pred  33792  sltval2  33853  sltres  33859  noseponlem  33861  nosepon  33862  nosepeq  33882  nosupbnd2lem1  33912  noinfbnd2lem1  33927  noetasuplem4  33933  noetainflem4  33937  btwnconn1lem13  34395  lineunray  34443  rankeq1o  34467  elicc3  34500  nn0prpw  34506  ordtoplem  34618  bj-snmoore  35278  irrdifflemf  35490  icorempo  35516  matunitlindflem1  35767  poimirlem1  35772  poimirlem14  35785  poimirlem16  35787  poimirlem19  35790  poimirlem23  35794  poimirlem25  35796  poimirlem26  35797  itg2addnclem3  35824  itgaddnclem2  35830  fdc  35897  ismgmOLD  36002  cvrval2  37282  cvrnbtwn2  37283  cvrnbtwn3  37284  cvlsupr3  37352  cvrat4  37451  2at0mat0  37533  dalawlem13  37891  isltrn2N  38128  trlator0  38179  cdleme22b  38349  dochkrshp  39394  dochkrshp4  39397  lcfl6  39508  lclkrlem2x  39538  metakunt6  40125  metakunt7  40126  metakunt11  40130  metakunt22  40141  isdomn5  40166  nnn1suc  40291  sn-00id  40379  remulid2  40410  infdesc  40475  fphpd  40633  jm2.23  40813  isdomn3  41024  dfsucon  41107  iunrelexp0  41278  ntrneineine1lem  41662  pm13.196a  42000  onfrALTlem5  42130  onfrALTlem3  42132  en3lpVD  42433  onfrALTlem5VD  42473  onfrALTlem3VD  42475  ax6e2ndeqVD  42497  ax6e2ndeqALT  42519  isosctrlem1ALT  42522  ndisj2  42567  limsupre2lem  43234  cncfiooicclem1  43403  iblcncfioo  43488  stoweidlem28  43538  sge0iunmpt  43925  afvfv0bi  44610  2ffzoeq  44787  iccpartiltu  44841  iccpartlt  44843  icceuelpartlem  44854  lighneallem4  45029  oddprmALTV  45106  evenprm2  45133  odd2prm2  45137  even3prm2  45138  upgrwlkupwlk  45269  copisnmnd  45330  pgrpgt2nabl  45669  islindeps  45761  lincext1  45762  lindslinindsimp2lem5  45770  snlindsntor  45779  ldepslinc  45817  m1modmmod  45834  rrx2linest  46055  line2ylem  46064  line2xlem  46066