Definition df-ne 2926

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

This definition is referenced by:  neii  2927  neir  2928  nne  2929  neneqd  2930  neqned  2932  eqneqall  2936  necon2bd  2941  necon1bd  2943  necon3d  2946  necon2d  2948  necon1bi  2953  necon1i  2958  necon3abid  2961  necon1bbid  2964  necon3bid  2969  necon3abii  2971  necon3bii  2977  neor  3017  neanior  3018  neorian  3020  nfne  3026  nfned  3027  nabbib  3028  nelb  3205  dfpss2  4039  dfdif3OLD  4069  n0f  4300  n0  4304  abn0  4336  2nreu  4395  raaan2  4472  ifnefalse  4488  snnzb  4670  raldifsni  4746  eqsn  4780  n0snor2el  4784  opthpr  4802  prneimg2  4806  opthprneg  4816  unissint  4922  iununi  5048  disji2  5076  opthneg  5424  otthne  5429  opab0  5497  xpcan  6125  xpcan2  6126  xpima  6131  unixpid  6232  unizlim  6431  dff14a  7207  orduniorsuc  7763  dflim3  7780  tfindsg  7794  nn0suc  7827  findsg  7830  resf1extb  7867  xpord2pred  8078  xpord2indlem  8080  frxp3  8084  suppvalbr  8097  frrlem14  8232  tz7.49  8367  oevn0  8433  fsetexb  8791  php  9121  1sdom  9144  fimaxg  9176  fiint  9216  fiintOLD  9217  wemapsolem  9442  card2on  9446  brwdomn0  9461  rankxplim2  9776  rankxplim3  9777  updjudhf  9827  carden2a  9862  enpr2  9898  dfackm  10061  fin1a2lem12  10305  ac6num  10373  zorn2lem4  10393  zorn2lem7  10396  brdom3  10422  iundom2g  10434  r1tskina  10676  ltlen  11217  uzm1  12773  xrnemnf  13019  xrnepnf  13020  ioo0  13273  ico0  13294  ioc0  13295  icc0  13296  fzne1  13507  elfznelfzo  13675  elfznelfzob  13676  injresinjlem  13690  fleqceilz  13758  fsuppmapnn0fiubex  13899  sq01  14132  hash1snb  14326  hashgt12el  14329  hashgt12el2  14330  hashfun  14344  hash2prde  14377  hashge2el2dif  14387  fundmge2nop0  14409  repswcshw  14718  cshw1  14728  incexc2  15745  sqrt2irr  16158  divalglem8  16311  ndvdssub  16320  algcvgblem  16488  lcmcllem  16507  lcmfunsnlem2  16551  isprm3  16594  isprm4  16595  2mulprm  16604  ramcl2lem  16921  cshwshashlem1  17007  cshwshash  17016  smndex2dnrinv  18789  sgrp2nmndlem3  18799  sgrp2nmndlem5  18803  symg2bas  19272  odfval  19411  dprdfeq0  19903  isnirred  20305  isirred2  20306  isnzr2  20403  isdomn5  20595  isdomn2OLD  20597  isdomn3  20600  drngmul0orOLD  20646  drngmuleq0  20648  sdrgacs  20686  lvecvs0or  21015  lvecvscan  21018  domnchr  21439  gsummoncoe1  22193  dmatmul  22382  mulmarep1gsum2  22459  mdetunilem8  22504  mp2pm2mplem4  22694  fvmptnn04if  22734  elcls  22958  opnnei  23005  ist0-3  23230  ist1-2  23232  dfconn2  23304  cnconn  23307  pthaus  23523  xkohaus  23538  hausflim  23866  cldsubg  23996  bcth  25227  ioorinv  25475  tdeglem4  25963  fta1b  26075  plydivex  26203  aalioulem3  26240  dvradcnv  26328  cxpcl  26581  recxpcl  26582  logrec  26671  isosctrlem2  26727  efrlim  26877  efrlimOLD  26878  muval2  27042  musum  27099  dchrelbas2  27146  dchrelbas4  27152  dchrfi  27164  dchrptlem3  27175  dchrsum2  27177  sumdchr2  27179  lgscllem  27213  2sqb  27341  2sqcoprm  27344  dchrvmasumiflem2  27411  rpvmasum2  27421  padicabv  27539  padicabvf  27540  padicabvcxp  27541  sltval2  27566  sltres  27572  noseponlem  27574  nosepon  27575  nosepeq  27595  nosupbnd2lem1  27625  noinfbnd2lem1  27640  noetasuplem4  27646  noetainflem4  27650  eln0s  28256  dfnns2  28266  tglowdim1i  28446  tgbtwnconn1  28520  colline  28594  colmid  28633  lmimid  28739  lmiisolem  28741  brbtwn2  28850  colinearalg  28855  axlowdimlem6  28892  axlowdimlem14  28900  axcontlem12  28920  incistruhgr  29024  umgr2edg1  29156  nb3grprlem1  29325  1egrvtxdg0  29457  vtxdginducedm1lem4  29488  wlkdlem4  29629  lfgriswlk  29632  pthdlem2  29713  wwlksnext  29838  clwwlknclwwlkdif  29923  clwlkclwwlklem2a4  29941  clwwisshclwwsn  29960  1wlkdlem4  30084  eupth2lem1  30162  eupth2lem3lem4  30175  frgr3vlem1  30217  frgr3vlem2  30218  3vfriswmgrlem  30221  4cycl2vnunb  30234  frgrncvvdeqlem8  30250  frgrregorufr  30269  frgrreg  30338  frgrregord013  30339  9p10ne21fool  30415  nvmul0or  30594  nmogtmnf  30714  hvmul0or  30969  hvmulcan  31016  hvmulcan2  31017  hiidge0  31042  bcsiALT  31123  shne0i  31392  nonbooli  31595  nmopgtmnf  31812  unopbd  31959  nmcfnlbi  31996  nmopcoi  32039  chirredi  32338  mdsymlem5  32351  sumdmdlem2  32363  n0nsnel  32459  disji2f  32521  aciunf1  32607  hashxpe  32753  sgn3da  32780  elrgspnlem2  33184  ply1dg3rt0irred  33519  extdgfialglem1  33665  sitgaddlemb  34322  plymulx  34522  bnj1109  34759  bnj1542  34830  bnj1253  34990  dff15  35057  lfuhgr3  35103  dfacycgr1  35127  subfacp1lem6  35168  cvmsdisj  35253  satffunlem1lem1  35385  satffunlem2lem1  35387  satffun  35392  btwnconn1lem13  36083  lineunray  36131  rankeq1o  36155  elicc3  36301  nn0prpw  36307  ordtoplem  36419  bj-snmoore  37097  irrdifflemf  37309  icorempo  37335  matunitlindflem1  37606  poimirlem1  37611  poimirlem14  37624  poimirlem16  37626  poimirlem19  37629  poimirlem23  37633  poimirlem25  37635  poimirlem26  37636  itg2addnclem3  37663  itgaddnclem2  37669  fdc  37735  ismgmOLD  37840  cvrval2  39263  cvrnbtwn2  39264  cvrnbtwn3  39265  cvlsupr3  39333  cvrat4  39432  2at0mat0  39514  dalawlem13  39872  isltrn2N  40109  trlator0  40160  cdleme22b  40330  dochkrshp  41375  dochkrshp4  41378  lcfl6  41489  lclkrlem2x  41519  hashnexinj  42111  rspcsbnea  42114  aks6d1c5  42122  nnn1suc  42249  expeqidd  42308  remullid  42417  fimgmcyc  42517  infdesc  42626  fphpd  42799  jm2.23  42979  dflim6  43247  onsucf1olem  43253  onov0suclim  43257  oenassex  43301  tfsconcatb0  43327  tfsconcat0b  43329  naddwordnexlem4  43384  safesnsupfilb  43401  faosnf0.11b  43410  dfsucon  43506  iunrelexp0  43685  ntrneineine1lem  44067  pm13.196a  44397  onfrALTlem5  44526  onfrALTlem3  44528  en3lpVD  44828  onfrALTlem5VD  44868  onfrALTlem3VD  44870  ax6e2ndeqVD  44892  ax6e2ndeqALT  44914  isosctrlem1ALT  44917  rext0  44922  dfac5prim  44974  modelac8prim  44976  permac8prim  44998  ndisj2  45039  limsupre2lem  45715  cncfiooicclem1  45884  iblcncfioo  45969  stoweidlem28  46019  sge0iunmpt  46409  n0nsn2el  47019  afvfv0bi  47146  2ffzoeq  47321  m1modmmod  47352  modm1p1ne  47364  iccpartiltu  47416  iccpartlt  47418  icceuelpartlem  47429  lighneallem4  47604  oddprmALTV  47681  evenprm2  47708  odd2prm2  47712  even3prm2  47713  upgrimpthslem2  47902  gpg5nbgrvtx03starlem1  48062  gpg5nbgrvtx03starlem2  48063  gpg5nbgrvtx03starlem3  48064  gpg5nbgrvtx13starlem1  48065  gpg5nbgrvtx13starlem2  48066  gpg5nbgrvtx13starlem3  48067  pg4cyclnex  48121  gpg5edgnedg  48124  upgrwlkupwlk  48134  copisnmnd  48163  pgrpgt2nabl  48360  islindeps  48448  lincext1  48449  lindslinindsimp2lem5  48457  snlindsntor  48466  ldepslinc  48504  rrx2linest  48737  line2ylem  48746  line2xlem  48748  oppcmndclem  49012