Definition df-ne 2965

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

This definition is referenced by:  neii  2966  neir  2967  nne  2968  neneqd  2969  neqned  2971  eqneqall  2975  necon2bd  2980  necon1bd  2982  necon3d  2985  necon2d  2987  necon1bi  2992  necon1i  2997  necon3abid  3000  necon1bbid  3003  necon3bid  3008  necon3abii  3010  necon3bii  3016  neor  3056  neanior  3057  neorian  3059  nfne  3067  nfned  3068  nabbi  3069  dfpss2  3951  dfdif3  3980  n0f  4192  2nreu  4274  raaan2  4345  ifnefalse  4360  snnzb  4526  raldifsni  4600  eqsn  4634  n0snor2el  4636  opthpr  4654  opthprneg  4667  unissint  4771  iununi  4885  disji2  4911  opthneg  5227  opab0  5290  xpcan  5871  xpcan2  5872  xpima  5877  unixpid  5971  unizlim  6143  dff14a  6851  orduniorsuc  7359  dflim3  7376  tfindsg  7389  nn0suc  7419  findsg  7422  suppvalbr  7634  wfrlem16  7771  tz7.49  7881  oevn0  7938  php  8493  1sdom  8512  fimaxg  8556  fiint  8586  wemapsolem  8805  card2on  8809  brwdomn0  8824  rankxplim2  9099  rankxplim3  9100  updjudhf  9150  carden2a  9185  dfackm  9382  fin1a2lem12  9627  ac6num  9695  zorn2lem4  9715  zorn2lem7  9718  brdom3  9744  iundom2g  9756  r1tskina  9998  1re  10435  ltlen  10537  uzm1  12087  xrnemnf  12326  xrnepnf  12327  ioo0  12576  ico0  12597  ioc0  12598  icc0  12599  elfznelfzo  12954  elfznelfzob  12955  injresinjlem  12969  fleqceilz  13034  fsuppmapnn0fiubex  13172  sq01  13398  hash1snb  13588  hashgt12el  13591  hashgt12el2  13592  hashfun  13605  hash2prde  13633  hashge2el2dif  13643  fundmge2nop0  13655  ccat1st1st  13785  swrdccatin1  13918  repswcshw  14030  cshw1  14040  incexc2  15047  sqrt2irr  15456  divalglem8  15605  ndvdssub  15614  algcvgblem  15771  lcmcllem  15790  lcmfunsnlem2  15834  isprm3  15877  isprm4  15878  2mulprm  15887  ramcl2lem  16195  cshwshashlem1  16279  cshwshash  16288  sgrp2nmndlem3  17875  sgrp2nmndlem5  17879  symg2bas  18281  odfval  18416  dprdfeq0  18888  isnirred  19167  isirred2  19168  drngmul0or  19240  drngmuleq0  19242  sdrgacs  19296  lvecvs0or  19596  lvecvscan  19599  isnzr2  19751  isdomn2  19787  gsummoncoe1  20169  domnchr  20375  dmatmul  20804  mulmarep1gsum2  20881  mdetunilem8  20926  mp2pm2mplem4  21115  fvmptnn04if  21155  elcls  21379  opnnei  21426  ist0-3  21651  ist1-2  21653  dfconn2  21725  cnconn  21728  pthaus  21944  xkohaus  21959  hausflim  22287  cldsubg  22416  bcth  23629  ioorinv  23874  tdeglem4  24351  fta1b  24460  plydivex  24583  aalioulem3  24620  dvradcnv  24706  cxpcl  24952  recxpcl  24953  logrec  25036  isosctrlem2  25092  efrlim  25243  muval2  25407  musum  25464  dchrelbas2  25509  dchrelbas4  25515  dchrfi  25527  dchrptlem3  25538  dchrsum2  25540  sumdchr2  25542  lgscllem  25576  2sqb  25704  2sqcoprm  25707  dchrvmasumiflem2  25774  rpvmasum2  25784  padicabv  25902  padicabvf  25903  padicabvcxp  25904  tglowdim1i  25983  tgbtwnconn1  26057  colline  26131  colmid  26170  lmimid  26276  lmiisolem  26278  brbtwn2  26388  colinearalg  26393  axlowdimlem6  26430  axlowdimlem14  26438  axcontlem12  26458  incistruhgr  26561  umgr2edg1  26690  nb3grprlem1  26859  1egrvtxdg0  26990  vtxdginducedm1lem4  27021  wlkdlem4  27167  lfgriswlk  27170  pthdlem2  27251  wwlksnext  27375  clwwlknclwwlkdif  27479  clwlkclwwlklem2a4  27497  clwwisshclwwsn  27525  1wlkdlem4  27663  eupth2lem1  27742  eupth2lem3lem4  27755  frgr3vlem1  27801  frgr3vlem2  27802  3vfriswmgrlem  27805  4cycl2vnunb  27818  frgrncvvdeqlem8  27834  frgrregorufr  27853  frgrreg  27945  frgrregord013  27946  9p10ne21fool  28021  nvmul0or  28198  nmogtmnf  28318  hvmul0or  28575  hvmulcan  28622  hvmulcan2  28623  hiidge0  28648  bcsiALT  28729  shne0i  29000  nonbooli  29203  nmopgtmnf  29420  unopbd  29567  nmcfnlbi  29604  nmopcoi  29647  chirredi  29946  mdsymlem5  29959  sumdmdlem2  29971  disji2f  30087  aciunf1  30164  hashxpe  30270  sitgaddlemb  31242  sgn3da  31436  plymulx  31455  bnj1109  31697  bnj1542  31767  bnj1253  31925  subfacp1lem6  32007  cvmsdisj  32092  frrlem14  32627  sltval2  32654  sltres  32660  noseponlem  32662  nosepon  32663  nosepeq  32680  nosupbnd2lem1  32706  noetalem3  32710  btwnconn1lem13  33051  lineunray  33099  rankeq1o  33123  elicc3  33156  nn0prpw  33162  ordtoplem  33273  bj-ismooredr2  33878  bj-snmoore  33881  icorempt2  34039  matunitlindflem1  34307  poimirlem1  34312  poimirlem14  34325  poimirlem16  34327  poimirlem19  34330  poimirlem23  34334  poimirlem25  34336  poimirlem26  34337  itg2addnclem3  34364  itgaddnclem2  34370  fdc  34440  ismgmOLD  34548  cvrval2  35833  cvrnbtwn2  35834  cvrnbtwn3  35835  cvlsupr3  35903  cvrat4  36002  2at0mat0  36084  dalawlem13  36442  isltrn2N  36679  trlator0  36730  cdleme22b  36900  dochkrshp  37945  dochkrshp4  37948  lcfl6  38059  lclkrlem2x  38089  nnn1suc  38572  fphpd  38787  jm2.23  38967  isdomn3  39178  iunrelexp0  39388  ntrneineine1lem  39775  pm13.196a  40140  onfrALTlem5  40272  onfrALTlem3  40274  en3lpVD  40575  onfrALTlem5VD  40615  onfrALTlem3VD  40617  ax6e2ndeqVD  40639  ax6e2ndeqALT  40661  isosctrlem1ALT  40664  ndisj2  40710  limsupre2lem  41415  cncfiooicclem1  41585  iblcncfioo  41672  stoweidlem28  41723  sge0iunmpt  42110  afvfv0bi  42736  2ffzoeq  42913  iccpartiltu  42933  iccpartlt  42935  icceuelpartlem  42946  lighneallem4  43117  oddprmALTV  43194  evenprm2  43221  odd2prm2  43225  even3prm2  43226  upgrwlkupwlk  43357  copisnmnd  43418  pgrpgt2nabl  43754  islindeps  43849  lincext1  43850  lindslinindsimp2lem5  43858  snlindsntor  43867  ldepslinc  43905  m1modmmod  43923  rrx2linest  44071  line2ylem  44080  line2xlem  44082