Definition df-ne 2960

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

This definition is used by:  neii  2961  neir  2962  nne  2963  neneqd  2964  neqned  2966  eqneqall  2970  necon2bd  2975  necon1bd  2977  necon3d  2980  necon2d  2982  necon1bi  2987  necon1i  2992  necon3abid  2995  necon1bbid  2998  necon3bid  3003  necon3abii  3005  necon3bii  3011  neor  3051  neanior  3052  neorian  3054  nfne  3062  nfned  3063  nabbib  3064  nelb  3242  dfpss2  4018  n0f  4299  n0  4303  abn0  4337  2nreu  4405  raaan2  4481  ifnefalse  4497  snnzb  4679  raldifsni  4758  eqsn  4788  n0snor2el  4791  opthpr  4809  prneimg2  4813  opthprneg  4823  unissint  4935  iununi  5062  disji2  5090  opthneg  5454  otthne  5459  opab0  5533  xpcan  6179  xpcan2  6180  xpima  6185  unixpid  6302  unizlim  6502  fvtp0  7226  dff14a  7294  dff15  7296  orduniorsuc  7862  dflim3  7879  tfindsg  7893  nn0suc  7927  findsg  7930  resf1extb  7967  xpord2pred  8186  xpord2indlem  8188  frxp3  8192  suppvalbr  8205  suppvalbrOLD  8206  frrlem14  8342  tz7.49  8480  oevn0  8548  fsetexb  8911  php  9247  1sdom  9271  fimaxg  9303  fiint  9343  wemapsolem  9568  card2on  9572  brwdomn0  9587  rankxplim2  9921  rankxplim3  9922  updjudhf  10036  carden2a  10071  enpr2  10107  dfackm  10269  fin1a2lem12  10513  ac6num  10581  zorn2lem4  10601  zorn2lem7  10604  brdom3  10631  iundom2g  10648  r1tskina  10891  ltlen  11435  uzm1  13023  xrnemnf  13270  xrnepnf  13271  ioo0  13525  ico0  13546  ioc0  13547  icc0  13548  fzne1  13762  elfznelfzo  13932  elfznelfzob  13933  injresinjlem  13949  fleqceilz  14018  fsuppmapnn0fiubex  14159  sq01  14393  hash1snb  14588  hashgt12el  14591  hashgt12el2  14592  hashfun  14606  hash2prde  14639  hashge2el2dif  14649  fundmge2nop0  14671  repswcshw  14988  cshw1  14998  sgn3da  15280  incexc2  16033  sqrt2irr  16443  divalglem8  16596  ndvdssub  16605  algcvgblem  16778  lcmcllem  16797  lcmfunsnlem2  16841  isprm3  16884  isprm4  16885  2mulprm  16894  ramcl2lem  17213  cshwshashlem1  17299  cshwshash  17308  smndex2dnrinv  19140  sgrp2nmndlem3  19150  sgrp2nmndlem5  19154  symg2bas  19634  odfval  19773  dprdfeq0  20265  isnirred  20677  isirred2  20678  isnzr2  20795  isdomn5  20989  isdomn3  20993  drngmuleq0  21047  sdrgacs  21085  lvecvs0or  21413  lvecvscan  21416  domnchr  21865  gsummoncoe1  22653  dmatmul  22839  mulmarep1gsum2  22916  mdetunilem8  22961  matunitlindflem1  23021  mp2pm2mplem4  23154  fvmptnn04if  23194  elcls  23418  opnnei  23465  ist0-3  23690  ist1-2  23692  dfconn2  23764  cnconn  23767  pthaus  23984  xkohaus  23999  hausflim  24327  cldsubg  24457  bcth  25677  ioorinv  25924  tdeglem4  26405  fta1b  26517  plymulidp  26630  plydivex  26645  rnplynfin  26657  plyconz  26658  aalioulem3  26688  dvradcnv  26775  cxpcl  27029  recxpcl  27030  logrec  27118  isosctrlem2  27174  efrlim  27324  muval2  27488  musum  27545  dchrelbas2  27591  dchrelbas4  27597  dchrfi  27609  dchrptlem3  27620  dchrsum2  27622  sumdchr2  27624  lgscllem  27658  2sqb  27786  2sqcoprm  27789  dchrvmasumiflem2  27856  rpvmasum2  27866  padicabv  27984  padicabvf  27985  padicabvcxp  27986  infdesc  27994  ltsval2  28040  ltsres  28046  noseponlem  28048  nosepon  28049  nosepeq  28069  nosupbnd2lem1  28099  noinfbnd2lem1  28114  noetasuplem4  28120  noetainflem4  28124  eln0s  28774  dfnns2  28785  bdayfinbndlem1  28880  tglowdim1i  28991  tgbtwnconn1  29065  colline  29145  colmid  29187  lmimid  29326  lmiisolem  29328  brbtwn2  29510  colinearalg  29515  axlowdimlem6  29552  axlowdimlem14  29560  axcontlem12  29580  incistruhgr  29684  lfuhgr3  29755  umgr2edg1  29819  nb3grprlem1  29988  1egrvtxdg0  30119  vtxdginducedm1lem4  30150  wlkdlem4  30291  lfgriswlk  30298  pthdlem2  30381  wwlksnext  30509  clwwlknclwwlkdif  30597  clwlkclwwlklem2a4  30615  clwwisshclwwsn  30634  1wlkdlem4  30758  dfacycgr1  30777  eupth2lem1  30846  eupth2lem3lem4  30859  frgr3vlem1  30901  frgr3vlem2  30902  3vfriswmgrlem  30905  4cycl2vnunb  30918  frgrncvvdeqlem8  30934  frgrregorufr  30953  frgrreg  31022  frgrregord013  31023  9p10ne21fool  31099  nvmul0or  31279  nmogtmnf  31399  hvmul0or  31654  hvmulcan  31701  hvmulcan2  31702  hiidge0  31727  bcsiALT  31808  shne0i  32077  nonbooli  32280  nmopgtmnf  32497  unopbd  32644  nmcfnlbi  32681  nmopcoi  32724  chirredi  33023  mdsymlem5  33036  sumdmdlem2  33048  n0nsnel  33180  disji2f  33240  aciunf1  33326  hashxpe  33466  elrgspnlem2  33871  ply1dg3rt0irred  34183  extdgfialglem1  34391  sitgaddlemb  35047  bnj1109  35484  bnj1542  35554  bnj1253  35714  erscottd  35842  maxssj0  36005  subfacp1lem6  36116  cvmsdisj  36201  satffunlem1lem1  36333  satffunlem2lem1  36335  satffun  36340  btwnconn1lem13  37041  lineunray  37089  rankeq1o  37109  nmulel1  37141  elicc3  37282  nn0prpw  37288  ordtoplem  37400  bj-snmoore  38224  irrdifflemf  38437  qdiffALT  38440  icorempo  38465  poimirlem1  38730  poimirlem14  38743  poimirlem16  38745  poimirlem19  38748  poimirlem23  38752  poimirlem25  38754  poimirlem26  38755  itg2addnclem3  38782  itgaddnclem2  38788  fdc  38870  ismgmOLD  38975  cvrval2  40522  cvrnbtwn2  40523  cvrnbtwn3  40524  cvlsupr3  40592  cvrat4  40691  2at0mat0  40773  dalawlem13  41131  isltrn2N  41368  trlator0  41419  cdleme22b  41589  dochkrshp  42634  dochkrshp4  42637  lcfl6  42748  lclkrlem2x  42778  hashnexinj  43369  rspcsbnea  43372  aks6d1c5  43380  nnn1suc  43522  expeqidd  43573  remullid  43676  fimgmcyc  43789  fphpd  44014  jm2.23  44194  dflim6  44456  onsucf1olem  44462  onov0suclim  44466  oenassex  44510  tfsconcatb0  44536  tfsconcat0b  44538  naddwordnexlem4  44593  safesnsupfilb  44609  faosnf0.11b  44618  dfsucon  44714  iunrelexp0  44892  ntrneineine1lem  45274  pm13.196a  45588  onfrALTlem5  45714  onfrALTlem3  45716  en3lpVD  46016  onfrALTlem5VD  46056  onfrALTlem3VD  46058  ax6e2ndeqVD  46080  ax6e2ndeqALT  46102  isosctrlem1ALT  46105  rext0  46110  dfac5prim  46173  modelac8prim  46175  permac8prim  46197  ndisj2  46271  limsupre2lem  46937  cncfiooicclem1  47106  iblcncfioo  47191  stoweidlem28  47241  sge0iunmpt  47631  chnerlem1  48095  n0nsn2el  48298  afvfv0bi  48425  2ffzoeq  48601  m1modmmod  48637  modm1p1ne  48649  iccpartiltu  48707  iccpartlt  48709  icceuelpartlem  48720  lighneallem4  48898  oddprmALTV  48988  evenprm2  49015  odd2prm2  49019  even3prm2  49020  upgrimpthslem2  49209  gpg5nbgrvtx03starlem1  49369  gpg5nbgrvtx03starlem2  49370  gpg5nbgrvtx03starlem3  49371  gpg5nbgrvtx13starlem1  49372  gpg5nbgrvtx13starlem2  49373  gpg5nbgrvtx13starlem3  49374  pg4cyclnex  49428  gpg5edgnedg  49431  upgrwlkupwlk  49441  copisnmnd  49469  pgrpgt2nabl  49681  islindeps  49768  lincext1  49769  lindslinindsimp2lem5  49777  snlindsntor  49786  ldepslinc  49824  rrx2linest  50057  line2ylem  50066  line2xlem  50068  oppcmndclem  50334