Definition df-ne 2937

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

This definition is referenced by:  neii  2938  neir  2939  nne  2940  neneqd  2941  neqned  2943  eqneqall  2947  necon2bd  2952  necon1bd  2954  necon3d  2957  necon2d  2959  necon1bi  2964  necon1i  2969  necon3abid  2972  necon1bbid  2975  necon3bid  2980  necon3abii  2982  necon3bii  2988  neor  3028  neanior  3029  neorian  3031  nfne  3037  nfned  3038  nabbib  3039  nelb  3217  dfpss2  4021  dfdif3OLD  4051  n0f  4279  n0  4283  abn0  4315  2nreu  4374  raaan2  4452  ifnefalse  4468  snnzb  4652  raldifsni  4730  eqsn  4762  n0snor2el  4766  opthpr  4784  prneimg2  4788  opthprneg  4798  unissint  4904  iununi  5030  disji2  5058  opthneg  5423  otthne  5428  opab0  5498  xpcan  6130  xpcan2  6131  xpima  6136  unixpid  6238  unizlim  6437  dff14a  7217  orduniorsuc  7773  dflim3  7790  tfindsg  7804  nn0suc  7838  findsg  7841  resf1extb  7878  xpord2pred  8087  xpord2indlem  8089  frxp3  8093  suppvalbr  8106  frrlem14  8242  tz7.49  8378  oevn0  8444  fsetexb  8805  php  9135  1sdom  9159  fimaxg  9191  fiint  9231  wemapsolem  9459  card2on  9463  brwdomn0  9478  rankxplim2  9799  rankxplim3  9800  updjudhf  9850  carden2a  9885  enpr2  9921  dfackm  10084  fin1a2lem12  10329  ac6num  10397  zorn2lem4  10417  zorn2lem7  10420  brdom3  10446  iundom2g  10458  r1tskina  10701  ltlen  11243  uzm1  12817  xrnemnf  13063  xrnepnf  13064  ioo0  13318  ico0  13339  ioc0  13340  icc0  13341  fzne1  13553  elfznelfzo  13723  elfznelfzob  13724  injresinjlem  13740  fleqceilz  13808  fsuppmapnn0fiubex  13949  sq01  14182  hash1snb  14376  hashgt12el  14379  hashgt12el2  14380  hashfun  14394  hash2prde  14427  hashge2el2dif  14437  fundmge2nop0  14459  repswcshw  14769  cshw1  14779  incexc2  15798  sqrt2irr  16211  divalglem8  16364  ndvdssub  16373  algcvgblem  16541  lcmcllem  16560  lcmfunsnlem2  16604  isprm3  16647  isprm4  16648  2mulprm  16657  ramcl2lem  16975  cshwshashlem1  17061  cshwshash  17070  smndex2dnrinv  18881  sgrp2nmndlem3  18891  sgrp2nmndlem5  18895  symg2bas  19362  odfval  19501  dprdfeq0  19993  isnirred  20394  isirred2  20395  isnzr2  20493  isdomn5  20685  isdomn2OLD  20687  isdomn3  20690  drngmul0orOLD  20736  drngmuleq0  20738  sdrgacs  20776  lvecvs0or  21104  lvecvscan  21107  domnchr  21510  gsummoncoe1  22297  dmatmul  22483  mulmarep1gsum2  22560  mdetunilem8  22605  mp2pm2mplem4  22795  fvmptnn04if  22835  elcls  23059  opnnei  23106  ist0-3  23331  ist1-2  23333  dfconn2  23405  cnconn  23408  pthaus  23624  xkohaus  23639  hausflim  23967  cldsubg  24097  bcth  25317  ioorinv  25564  tdeglem4  26046  fta1b  26158  plydivex  26284  aalioulem3  26321  dvradcnv  26407  cxpcl  26659  recxpcl  26660  logrec  26748  isosctrlem2  26804  efrlim  26954  muval2  27118  musum  27175  dchrelbas2  27221  dchrelbas4  27227  dchrfi  27239  dchrptlem3  27250  dchrsum2  27252  sumdchr2  27254  lgscllem  27288  2sqb  27416  2sqcoprm  27419  dchrvmasumiflem2  27486  rpvmasum2  27496  padicabv  27614  padicabvf  27615  padicabvcxp  27616  ltsval2  27640  ltsres  27646  noseponlem  27648  nosepon  27649  nosepeq  27669  nosupbnd2lem1  27699  noinfbnd2lem1  27714  noetasuplem4  27720  noetainflem4  27724  eln0s  28373  dfnns2  28384  bdayfinbndlem1  28479  tglowdim1i  28589  tgbtwnconn1  28663  colline  28737  colmid  28776  lmimid  28882  lmiisolem  28884  brbtwn2  28994  colinearalg  28999  axlowdimlem6  29036  axlowdimlem14  29044  axcontlem12  29064  incistruhgr  29168  umgr2edg1  29300  nb3grprlem1  29469  1egrvtxdg0  29600  vtxdginducedm1lem4  29631  wlkdlem4  29772  lfgriswlk  29775  pthdlem2  29856  wwlksnext  29981  clwwlknclwwlkdif  30069  clwlkclwwlklem2a4  30087  clwwisshclwwsn  30106  1wlkdlem4  30230  eupth2lem1  30308  eupth2lem3lem4  30321  frgr3vlem1  30363  frgr3vlem2  30364  3vfriswmgrlem  30367  4cycl2vnunb  30380  frgrncvvdeqlem8  30396  frgrregorufr  30415  frgrreg  30484  frgrregord013  30485  9p10ne21fool  30561  nvmul0or  30741  nmogtmnf  30861  hvmul0or  31116  hvmulcan  31163  hvmulcan2  31164  hiidge0  31189  bcsiALT  31270  shne0i  31539  nonbooli  31742  nmopgtmnf  31959  unopbd  32106  nmcfnlbi  32143  nmopcoi  32186  chirredi  32485  mdsymlem5  32498  sumdmdlem2  32510  n0nsnel  32605  disji2f  32668  aciunf1  32757  hashxpe  32901  sgn3da  32928  elrgspnlem2  33326  ply1dg3rt0irred  33677  extdgfialglem1  33886  sitgaddlemb  34542  plymulx  34742  bnj1109  34982  bnj1542  35052  bnj1253  35212  dff15  35278  lfuhgr3  35361  dfacycgr1  35385  subfacp1lem6  35426  cvmsdisj  35511  satffunlem1lem1  35643  satffunlem2lem1  35645  satffun  35650  btwnconn1lem13  36340  lineunray  36388  rankeq1o  36412  elicc3  36558  nn0prpw  36564  ordtoplem  36676  bj-snmoore  37484  irrdifflemf  37698  qdiffALT  37701  icorempo  37726  matunitlindflem1  37996  poimirlem1  38001  poimirlem14  38014  poimirlem16  38016  poimirlem19  38019  poimirlem23  38023  poimirlem25  38025  poimirlem26  38026  itg2addnclem3  38053  itgaddnclem2  38059  fdc  38125  ismgmOLD  38230  cvrval2  39779  cvrnbtwn2  39780  cvrnbtwn3  39781  cvlsupr3  39849  cvrat4  39948  2at0mat0  40030  dalawlem13  40388  isltrn2N  40625  trlator0  40676  cdleme22b  40846  dochkrshp  41891  dochkrshp4  41894  lcfl6  42005  lclkrlem2x  42035  hashnexinj  42626  rspcsbnea  42629  aks6d1c5  42637  nnn1suc  42762  expeqidd  42815  remullid  42924  fimgmcyc  43033  infdesc  43106  fphpd  43274  jm2.23  43454  dflim6  43722  onsucf1olem  43728  onov0suclim  43732  oenassex  43776  tfsconcatb0  43802  tfsconcat0b  43804  naddwordnexlem4  43859  safesnsupfilb  43875  faosnf0.11b  43884  dfsucon  43980  iunrelexp0  44159  ntrneineine1lem  44541  pm13.196a  44871  onfrALTlem5  44999  onfrALTlem3  45001  en3lpVD  45301  onfrALTlem5VD  45341  onfrALTlem3VD  45343  ax6e2ndeqVD  45365  ax6e2ndeqALT  45387  isosctrlem1ALT  45390  rext0  45395  dfac5prim  45447  modelac8prim  45449  permac8prim  45471  ndisj2  45512  limsupre2lem  46179  cncfiooicclem1  46348  iblcncfioo  46433  stoweidlem28  46483  sge0iunmpt  46873  chnerlem1  47339  n0nsn2el  47500  afvfv0bi  47627  2ffzoeq  47803  m1modmmod  47839  modm1p1ne  47851  iccpartiltu  47909  iccpartlt  47911  icceuelpartlem  47922  lighneallem4  48100  oddprmALTV  48190  evenprm2  48217  odd2prm2  48221  even3prm2  48222  upgrimpthslem2  48411  gpg5nbgrvtx03starlem1  48571  gpg5nbgrvtx03starlem2  48572  gpg5nbgrvtx03starlem3  48573  gpg5nbgrvtx13starlem1  48574  gpg5nbgrvtx13starlem2  48575  gpg5nbgrvtx13starlem3  48576  pg4cyclnex  48630  gpg5edgnedg  48633  upgrwlkupwlk  48643  copisnmnd  48672  pgrpgt2nabl  48869  islindeps  48956  lincext1  48957  lindslinindsimp2lem5  48965  snlindsntor  48974  ldepslinc  49012  rrx2linest  49245  line2ylem  49254  line2xlem  49256  oppcmndclem  49519