Definition df-ne 2957

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

This definition is referenced by:  neii  2958  neir  2959  nne  2960  neneqd  2961  neqned  2963  eqneqall  2967  necon2bd  2972  necon1bd  2974  necon3d  2977  necon2d  2979  necon1bi  2984  necon1i  2989  necon3abid  2992  necon1bbid  2995  necon3bid  3000  necon3abii  3002  necon3bii  3008  neor  3048  neanior  3049  neorian  3051  nfne  3059  nfned  3060  nabbib  3061  nelb  3239  dfpss2  4041  dfdif3OLD  4072  n0f  4302  n0  4306  abn0  4340  2nreu  4408  raaan2  4482  ifnefalse  4498  snnzb  4683  raldifsni  4762  eqsn  4794  n0snor2el  4797  opthpr  4815  prneimg2  4819  opthprneg  4829  unissint  4936  iununi  5064  disji2  5092  opthneg  5463  otthne  5468  opab0  5539  xpcan  6174  xpcan2  6175  xpima  6180  unixpid  6285  unizlim  6485  dff14a  7268  orduniorsuc  7825  dflim3  7842  tfindsg  7856  nn0suc  7890  findsg  7893  resf1extb  7930  xpord2pred  8140  xpord2indlem  8142  frxp3  8146  suppvalbr  8159  frrlem14  8295  tz7.49  8431  oevn0  8499  fsetexb  8860  php  9190  1sdom  9214  fimaxg  9246  fiint  9285  wemapsolem  9511  card2on  9515  brwdomn0  9530  rankxplim2  9851  rankxplim3  9852  updjudhf  9916  carden2a  9951  enpr2  9987  dfackm  10149  fin1a2lem12  10394  ac6num  10462  zorn2lem4  10482  zorn2lem7  10485  brdom3  10511  iundom2g  10523  r1tskina  10766  ltlen  11310  uzm1  12895  xrnemnf  13141  xrnepnf  13142  ioo0  13396  ico0  13417  ioc0  13418  icc0  13419  fzne1  13631  elfznelfzo  13801  elfznelfzob  13802  injresinjlem  13818  fleqceilz  13886  fsuppmapnn0fiubex  14027  sq01  14260  hash1snb  14455  hashgt12el  14458  hashgt12el2  14459  hashfun  14473  hash2prde  14506  hashge2el2dif  14516  fundmge2nop0  14538  repswcshw  14848  cshw1  14858  sgn3da  15137  incexc2  15891  sqrt2irr  16304  divalglem8  16457  ndvdssub  16466  algcvgblem  16634  lcmcllem  16653  lcmfunsnlem2  16697  isprm3  16740  isprm4  16741  2mulprm  16750  ramcl2lem  17068  cshwshashlem1  17154  cshwshash  17163  smndex2dnrinv  18976  sgrp2nmndlem3  18986  sgrp2nmndlem5  18990  symg2bas  19462  odfval  19601  dprdfeq0  20093  isnirred  20501  isirred2  20502  isnzr2  20600  isdomn5  20794  isdomn3  20798  drngmuleq0  20846  sdrgacs  20883  lvecvs0or  21211  lvecvscan  21214  domnchr  21661  gsummoncoe1  22447  dmatmul  22633  mulmarep1gsum2  22710  mdetunilem8  22755  mp2pm2mplem4  22945  fvmptnn04if  22985  elcls  23209  opnnei  23256  ist0-3  23481  ist1-2  23483  dfconn2  23555  cnconn  23558  pthaus  23774  xkohaus  23789  hausflim  24117  cldsubg  24247  bcth  25467  ioorinv  25714  tdeglem4  26196  fta1b  26308  plymulidp  26422  plydivex  26437  aalioulem3  26474  dvradcnv  26560  cxpcl  26815  recxpcl  26816  logrec  26904  isosctrlem2  26960  efrlim  27110  muval2  27274  musum  27331  dchrelbas2  27377  dchrelbas4  27383  dchrfi  27395  dchrptlem3  27406  dchrsum2  27408  sumdchr2  27410  lgscllem  27444  2sqb  27572  2sqcoprm  27575  dchrvmasumiflem2  27642  rpvmasum2  27652  padicabv  27770  padicabvf  27771  padicabvcxp  27772  ltsval2  27796  ltsres  27802  noseponlem  27804  nosepon  27805  nosepeq  27825  nosupbnd2lem1  27855  noinfbnd2lem1  27870  noetasuplem4  27876  noetainflem4  27880  eln0s  28530  dfnns2  28541  bdayfinbndlem1  28636  tglowdim1i  28746  tgbtwnconn1  28820  colline  28899  colmid  28941  lmimid  29077  lmiisolem  29079  brbtwn2  29221  colinearalg  29226  axlowdimlem6  29263  axlowdimlem14  29271  axcontlem12  29291  incistruhgr  29395  umgr2edg1  29527  nb3grprlem1  29696  1egrvtxdg0  29827  vtxdginducedm1lem4  29858  wlkdlem4  29999  lfgriswlk  30002  pthdlem2  30083  wwlksnext  30208  clwwlknclwwlkdif  30296  clwlkclwwlklem2a4  30314  clwwisshclwwsn  30333  1wlkdlem4  30457  eupth2lem1  30535  eupth2lem3lem4  30548  frgr3vlem1  30590  frgr3vlem2  30591  3vfriswmgrlem  30594  4cycl2vnunb  30607  frgrncvvdeqlem8  30623  frgrregorufr  30642  frgrreg  30711  frgrregord013  30712  9p10ne21fool  30788  nvmul0or  30968  nmogtmnf  31088  hvmul0or  31343  hvmulcan  31390  hvmulcan2  31391  hiidge0  31416  bcsiALT  31497  shne0i  31766  nonbooli  31969  nmopgtmnf  32186  unopbd  32333  nmcfnlbi  32370  nmopcoi  32413  chirredi  32712  mdsymlem5  32725  sumdmdlem2  32737  n0nsnel  32827  disji2f  32888  aciunf1  32974  hashxpe  33118  elrgspnlem2  33529  ply1dg3rt0irred  33840  extdgfialglem1  34048  sitgaddlemb  34704  bnj1109  35141  bnj1542  35211  bnj1253  35371  dff15  35437  lfuhgr3  35566  dfacycgr1  35590  subfacp1lem6  35631  cvmsdisj  35716  satffunlem1lem1  35848  satffunlem2lem1  35850  satffun  35855  btwnconn1lem13  36545  lineunray  36593  rankeq1o  36617  elicc3  36772  nn0prpw  36778  ordtoplem  36890  bj-snmoore  37699  irrdifflemf  37913  qdiffALT  37916  icorempo  37941  matunitlindflem1  38211  poimirlem1  38216  poimirlem14  38229  poimirlem16  38231  poimirlem19  38234  poimirlem23  38238  poimirlem25  38240  poimirlem26  38241  itg2addnclem3  38268  itgaddnclem2  38274  fdc  38340  ismgmOLD  38445  cvrval2  39994  cvrnbtwn2  39995  cvrnbtwn3  39996  cvlsupr3  40064  cvrat4  40163  2at0mat0  40245  dalawlem13  40603  isltrn2N  40840  trlator0  40891  cdleme22b  41061  dochkrshp  42106  dochkrshp4  42109  lcfl6  42220  lclkrlem2x  42250  hashnexinj  42841  rspcsbnea  42844  aks6d1c5  42852  nnn1suc  42979  expeqidd  43032  remullid  43141  fimgmcyc  43250  infdesc  43323  fphpd  43491  jm2.23  43671  dflim6  43939  onsucf1olem  43945  onov0suclim  43949  oenassex  43993  tfsconcatb0  44019  tfsconcat0b  44021  naddwordnexlem4  44076  safesnsupfilb  44092  faosnf0.11b  44101  dfsucon  44197  iunrelexp0  44376  ntrneineine1lem  44758  pm13.196a  45072  onfrALTlem5  45199  onfrALTlem3  45201  en3lpVD  45501  onfrALTlem5VD  45541  onfrALTlem3VD  45543  ax6e2ndeqVD  45565  ax6e2ndeqALT  45587  isosctrlem1ALT  45590  rext0  45595  dfac5prim  45647  modelac8prim  45649  permac8prim  45671  ndisj2  45719  limsupre2lem  46386  cncfiooicclem1  46555  iblcncfioo  46640  stoweidlem28  46690  sge0iunmpt  47080  chnerlem1  47546  n0nsn2el  47707  afvfv0bi  47834  2ffzoeq  48010  m1modmmod  48046  modm1p1ne  48058  iccpartiltu  48116  iccpartlt  48118  icceuelpartlem  48129  lighneallem4  48307  oddprmALTV  48397  evenprm2  48424  odd2prm2  48428  even3prm2  48429  upgrimpthslem2  48618  gpg5nbgrvtx03starlem1  48778  gpg5nbgrvtx03starlem2  48779  gpg5nbgrvtx03starlem3  48780  gpg5nbgrvtx13starlem1  48781  gpg5nbgrvtx13starlem2  48782  gpg5nbgrvtx13starlem3  48783  pg4cyclnex  48837  gpg5edgnedg  48840  upgrwlkupwlk  48850  copisnmnd  48879  pgrpgt2nabl  49091  islindeps  49178  lincext1  49179  lindslinindsimp2lem5  49187  snlindsntor  49196  ldepslinc  49234  rrx2linest  49467  line2ylem  49476  line2xlem  49478  oppcmndclem  49740