Definition df-ne 2942

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 2941	. 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  2943  neir  2944  nne  2945  neneqd  2946  neqned  2948  eqneqall  2952  necon2bd  2957  necon1bd  2959  necon3d  2962  necon2d  2964  necon1bi  2970  necon1i  2975  necon3abid  2978  necon1bbid  2981  necon3bid  2986  necon3abii  2988  necon3bii  2994  neor  3035  neanior  3036  neorian  3038  nfne  3044  nfned  3045  nabbib  3046  nelb  3232  nelbOLD  3233  dfpss2  4086  dfdif3  4115  n0f  4343  n0  4347  abn0  4381  2nreu  4442  raaan2  4525  ifnefalse  4541  snnzb  4723  raldifsni  4799  eqsn  4833  n0snor2el  4835  opthpr  4853  opthprneg  4866  unissint  4977  iununi  5103  disji2  5131  opthneg  5482  otthne  5487  opab0  5555  xpcan  6176  xpcan2  6177  xpima  6182  unixpid  6284  unizlim  6488  dff14a  7269  orduniorsuc  7818  dflim3  7836  tfindsg  7850  nn0suc  7886  findsg  7890  xpord2pred  8131  xpord2indlem  8133  frxp3  8137  suppvalbr  8150  frrlem14  8284  wfrlem16OLD  8324  tz7.49  8445  oevn0  8515  fsetexb  8858  php  9210  phpOLD  9222  1sdom  9248  1sdomOLD  9249  fimaxg  9290  fiint  9324  wemapsolem  9545  card2on  9549  brwdomn0  9564  rankxplim2  9875  rankxplim3  9876  updjudhf  9926  carden2a  9961  enpr2  9997  dfackm  10161  fin1a2lem12  10406  ac6num  10474  zorn2lem4  10494  zorn2lem7  10497  brdom3  10523  iundom2g  10535  r1tskina  10777  1re  11214  ltlen  11315  uzm1  12860  xrnemnf  13097  xrnepnf  13098  ioo0  13349  ico0  13370  ioc0  13371  icc0  13372  elfznelfzo  13737  elfznelfzob  13738  injresinjlem  13752  fleqceilz  13819  fsuppmapnn0fiubex  13957  sq01  14188  hash1snb  14379  hashgt12el  14382  hashgt12el2  14383  hashfun  14397  hash2prde  14431  hashge2el2dif  14441  fundmge2nop0  14453  repswcshw  14762  cshw1  14772  incexc2  15784  sqrt2irr  16192  divalglem8  16343  ndvdssub  16352  algcvgblem  16514  lcmcllem  16533  lcmfunsnlem2  16577  isprm3  16620  isprm4  16621  2mulprm  16630  ramcl2lem  16942  cshwshashlem1  17029  cshwshash  17038  smndex2dnrinv  18796  sgrp2nmndlem3  18806  sgrp2nmndlem5  18810  symg2bas  19260  odfval  19400  dprdfeq0  19892  isnirred  20234  isirred2  20235  isnzr2  20297  drngmul0or  20386  drngmuleq0  20388  sdrgacs  20417  lvecvs0or  20721  lvecvscan  20724  isdomn2  20915  isdomn5  20917  domnchr  21084  gsummoncoe1  21828  dmatmul  21999  mulmarep1gsum2  22076  mdetunilem8  22121  mp2pm2mplem4  22311  fvmptnn04if  22351  elcls  22577  opnnei  22624  ist0-3  22849  ist1-2  22851  dfconn2  22923  cnconn  22926  pthaus  23142  xkohaus  23157  hausflim  23485  cldsubg  23615  bcth  24846  ioorinv  25093  tdeglem4  25577  tdeglem4OLD  25578  fta1b  25687  plydivex  25810  aalioulem3  25847  dvradcnv  25933  cxpcl  26182  recxpcl  26183  logrec  26268  isosctrlem2  26324  efrlim  26474  muval2  26638  musum  26695  dchrelbas2  26740  dchrelbas4  26746  dchrfi  26758  dchrptlem3  26769  dchrsum2  26771  sumdchr2  26773  lgscllem  26807  2sqb  26935  2sqcoprm  26938  dchrvmasumiflem2  27005  rpvmasum2  27015  padicabv  27133  padicabvf  27134  padicabvcxp  27135  sltval2  27159  sltres  27165  noseponlem  27167  nosepon  27168  nosepeq  27188  nosupbnd2lem1  27218  noinfbnd2lem1  27233  noetasuplem4  27239  noetainflem4  27243  tglowdim1i  27752  tgbtwnconn1  27826  colline  27900  colmid  27939  lmimid  28045  lmiisolem  28047  brbtwn2  28163  colinearalg  28168  axlowdimlem6  28205  axlowdimlem14  28213  axcontlem12  28233  incistruhgr  28339  umgr2edg1  28468  nb3grprlem1  28637  1egrvtxdg0  28768  vtxdginducedm1lem4  28799  wlkdlem4  28942  lfgriswlk  28945  pthdlem2  29025  wwlksnext  29147  clwwlknclwwlkdif  29232  clwlkclwwlklem2a4  29250  clwwisshclwwsn  29269  1wlkdlem4  29393  eupth2lem1  29471  eupth2lem3lem4  29484  frgr3vlem1  29526  frgr3vlem2  29527  3vfriswmgrlem  29530  4cycl2vnunb  29543  frgrncvvdeqlem8  29559  frgrregorufr  29578  frgrreg  29647  frgrregord013  29648  9p10ne21fool  29724  nvmul0or  29903  nmogtmnf  30023  hvmul0or  30278  hvmulcan  30325  hvmulcan2  30326  hiidge0  30351  bcsiALT  30432  shne0i  30701  nonbooli  30904  nmopgtmnf  31121  unopbd  31268  nmcfnlbi  31305  nmopcoi  31348  chirredi  31647  mdsymlem5  31660  sumdmdlem2  31672  disji2f  31808  aciunf1  31888  fzne1  31999  hashxpe  32019  sitgaddlemb  33347  sgn3da  33540  plymulx  33559  bnj1109  33797  bnj1542  33868  bnj1253  34028  dff15  34087  lfuhgr3  34110  dfacycgr1  34135  subfacp1lem6  34176  cvmsdisj  34261  satffunlem1lem1  34393  satffunlem2lem1  34395  satffun  34400  btwnconn1lem13  35071  lineunray  35119  rankeq1o  35143  elicc3  35202  nn0prpw  35208  ordtoplem  35320  bj-snmoore  35994  irrdifflemf  36206  icorempo  36232  matunitlindflem1  36484  poimirlem1  36489  poimirlem14  36502  poimirlem16  36504  poimirlem19  36507  poimirlem23  36511  poimirlem25  36513  poimirlem26  36514  itg2addnclem3  36541  itgaddnclem2  36547  fdc  36613  ismgmOLD  36718  cvrval2  38144  cvrnbtwn2  38145  cvrnbtwn3  38146  cvlsupr3  38214  cvrat4  38314  2at0mat0  38396  dalawlem13  38754  isltrn2N  38991  trlator0  39042  cdleme22b  39212  dochkrshp  40257  dochkrshp4  40260  lcfl6  40371  lclkrlem2x  40401  metakunt6  40990  metakunt7  40991  metakunt11  40995  metakunt22  41006  nnn1suc  41180  remullid  41306  infdesc  41385  fphpd  41554  jm2.23  41735  isdomn3  41946  dflim6  42014  onsucf1olem  42020  onov0suclim  42024  oenassex  42068  tfsconcatb0  42094  tfsconcat0b  42096  naddwordnexlem4  42152  safesnsupfilb  42169  faosnf0.11b  42178  dfsucon  42274  iunrelexp0  42453  ntrneineine1lem  42835  pm13.196a  43173  onfrALTlem5  43303  onfrALTlem3  43305  en3lpVD  43606  onfrALTlem5VD  43646  onfrALTlem3VD  43648  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692  isosctrlem1ALT  43695  ndisj2  43738  limsupre2lem  44440  cncfiooicclem1  44609  iblcncfioo  44694  stoweidlem28  44744  sge0iunmpt  45134  n0nsn2el  45735  afvfv0bi  45860  2ffzoeq  46036  iccpartiltu  46090  iccpartlt  46092  icceuelpartlem  46103  lighneallem4  46278  oddprmALTV  46355  evenprm2  46382  odd2prm2  46386  even3prm2  46387  upgrwlkupwlk  46518  copisnmnd  46579  pgrpgt2nabl  47042  islindeps  47134  lincext1  47135  lindslinindsimp2lem5  47143  snlindsntor  47152  ldepslinc  47190  m1modmmod  47207  rrx2linest  47428  line2ylem  47437  line2xlem  47439