Definition df-ne 2956

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

This definition is used by:  neii  2957  neir  2958  nne  2959  neneqd  2960  neqned  2962  eqneqall  2966  necon2bd  2971  necon1bd  2973  necon3d  2976  necon2d  2978  necon1bi  2983  necon1i  2988  necon3abid  2991  necon1bbid  2994  necon3bid  2999  necon3abii  3001  necon3bii  3007  neor  3047  neanior  3048  neorian  3050  nfne  3058  nfned  3059  nabbib  3060  nelb  3238  dfpss2  4015  n0f  4295  n0  4299  abn0  4333  2nreu  4401  raaan2  4477  ifnefalse  4493  snnzb  4678  raldifsni  4757  eqsn  4789  n0snor2el  4792  opthpr  4810  prneimg2  4814  opthprneg  4824  unissint  4931  iununi  5058  disji2  5086  opthneg  5449  otthne  5454  opab0  5528  xpcan  6167  xpcan2  6168  xpima  6173  unixpid  6287  unizlim  6487  fvtp0  7206  dff14a  7274  dff15  7276  orduniorsuc  7841  dflim3  7858  tfindsg  7872  nn0suc  7906  findsg  7909  resf1extb  7946  xpord2pred  8162  xpord2indlem  8164  frxp3  8168  suppvalbr  8181  frrlem14  8317  tz7.49  8455  oevn0  8523  fsetexb  8886  php  9222  1sdom  9246  fimaxg  9278  fiint  9318  wemapsolem  9544  card2on  9548  brwdomn0  9563  rankxplim2  9897  rankxplim3  9898  updjudhf  10012  carden2a  10047  enpr2  10083  dfackm  10245  fin1a2lem12  10489  ac6num  10557  zorn2lem4  10577  zorn2lem7  10580  brdom3  10607  iundom2g  10624  r1tskina  10867  ltlen  11411  uzm1  12999  xrnemnf  13246  xrnepnf  13247  ioo0  13501  ico0  13522  ioc0  13523  icc0  13524  fzne1  13738  elfznelfzo  13908  elfznelfzob  13909  injresinjlem  13925  fleqceilz  13994  fsuppmapnn0fiubex  14135  sq01  14369  hash1snb  14564  hashgt12el  14567  hashgt12el2  14568  hashfun  14582  hash2prde  14615  hashge2el2dif  14625  fundmge2nop0  14647  repswcshw  14963  cshw1  14973  sgn3da  15254  incexc2  16007  sqrt2irr  16417  divalglem8  16570  ndvdssub  16579  algcvgblem  16752  lcmcllem  16771  lcmfunsnlem2  16815  isprm3  16858  isprm4  16859  2mulprm  16868  ramcl2lem  17187  cshwshashlem1  17273  cshwshash  17282  smndex2dnrinv  19114  sgrp2nmndlem3  19124  sgrp2nmndlem5  19128  symg2bas  19607  odfval  19746  dprdfeq0  20238  isnirred  20650  isirred2  20651  isnzr2  20768  isdomn5  20962  isdomn3  20966  drngmuleq0  21020  sdrgacs  21058  lvecvs0or  21386  lvecvscan  21389  domnchr  21838  gsummoncoe1  22626  dmatmul  22812  mulmarep1gsum2  22889  mdetunilem8  22934  matunitlindflem1  22994  mp2pm2mplem4  23127  fvmptnn04if  23167  elcls  23391  opnnei  23438  ist0-3  23663  ist1-2  23665  dfconn2  23737  cnconn  23740  pthaus  23957  xkohaus  23972  hausflim  24300  cldsubg  24430  bcth  25650  ioorinv  25897  tdeglem4  26378  fta1b  26490  plymulidp  26603  plydivex  26618  rnplynfin  26630  plyconz  26631  aalioulem3  26661  dvradcnv  26748  cxpcl  27002  recxpcl  27003  logrec  27091  isosctrlem2  27147  efrlim  27297  muval2  27461  musum  27518  dchrelbas2  27564  dchrelbas4  27570  dchrfi  27582  dchrptlem3  27593  dchrsum2  27595  sumdchr2  27597  lgscllem  27631  2sqb  27759  2sqcoprm  27762  dchrvmasumiflem2  27829  rpvmasum2  27839  padicabv  27957  padicabvf  27958  padicabvcxp  27959  infdesc  27967  ltsval2  28013  ltsres  28019  noseponlem  28021  nosepon  28022  nosepeq  28042  nosupbnd2lem1  28072  noinfbnd2lem1  28087  noetasuplem4  28093  noetainflem4  28097  eln0s  28747  dfnns2  28758  bdayfinbndlem1  28853  tglowdim1i  28964  tgbtwnconn1  29038  colline  29118  colmid  29160  lmimid  29299  lmiisolem  29301  brbtwn2  29483  colinearalg  29488  axlowdimlem6  29525  axlowdimlem14  29533  axcontlem12  29553  incistruhgr  29657  lfuhgr3  29728  umgr2edg1  29792  nb3grprlem1  29961  1egrvtxdg0  30092  vtxdginducedm1lem4  30123  wlkdlem4  30264  lfgriswlk  30271  pthdlem2  30354  wwlksnext  30482  clwwlknclwwlkdif  30570  clwlkclwwlklem2a4  30588  clwwisshclwwsn  30607  1wlkdlem4  30731  dfacycgr1  30750  eupth2lem1  30819  eupth2lem3lem4  30832  frgr3vlem1  30874  frgr3vlem2  30875  3vfriswmgrlem  30878  4cycl2vnunb  30891  frgrncvvdeqlem8  30907  frgrregorufr  30926  frgrreg  30995  frgrregord013  30996  9p10ne21fool  31072  nvmul0or  31252  nmogtmnf  31372  hvmul0or  31627  hvmulcan  31674  hvmulcan2  31675  hiidge0  31700  bcsiALT  31781  shne0i  32050  nonbooli  32253  nmopgtmnf  32470  unopbd  32617  nmcfnlbi  32654  nmopcoi  32697  chirredi  32996  mdsymlem5  33009  sumdmdlem2  33021  n0nsnel  33153  disji2f  33213  aciunf1  33299  hashxpe  33441  elrgspnlem2  33846  ply1dg3rt0irred  34158  extdgfialglem1  34366  sitgaddlemb  35022  bnj1109  35459  bnj1542  35529  bnj1253  35689  subfacp1lem6  35992  cvmsdisj  36077  satffunlem1lem1  36209  satffunlem2lem1  36211  satffun  36216  btwnconn1lem13  36906  lineunray  36954  rankeq1o  36974  nmulel1  37006  elicc3  37147  nn0prpw  37153  ordtoplem  37265  bj-snmoore  38076  irrdifflemf  38289  qdiffALT  38292  icorempo  38317  poimirlem1  38582  poimirlem14  38595  poimirlem16  38597  poimirlem19  38600  poimirlem23  38604  poimirlem25  38606  poimirlem26  38607  itg2addnclem3  38634  itgaddnclem2  38640  fdc  38722  ismgmOLD  38827  cvrval2  40374  cvrnbtwn2  40375  cvrnbtwn3  40376  cvlsupr3  40444  cvrat4  40543  2at0mat0  40625  dalawlem13  40983  isltrn2N  41220  trlator0  41271  cdleme22b  41441  dochkrshp  42486  dochkrshp4  42489  lcfl6  42600  lclkrlem2x  42630  hashnexinj  43221  rspcsbnea  43224  aks6d1c5  43232  nnn1suc  43374  expeqidd  43425  remullid  43528  fimgmcyc  43641  fphpd  43865  jm2.23  44045  dflim6  44308  onsucf1olem  44314  onov0suclim  44318  oenassex  44362  tfsconcatb0  44388  tfsconcat0b  44390  naddwordnexlem4  44445  safesnsupfilb  44461  faosnf0.11b  44470  dfsucon  44566  iunrelexp0  44744  ntrneineine1lem  45126  pm13.196a  45440  onfrALTlem5  45567  onfrALTlem3  45569  en3lpVD  45869  onfrALTlem5VD  45909  onfrALTlem3VD  45911  ax6e2ndeqVD  45933  ax6e2ndeqALT  45955  isosctrlem1ALT  45958  rext0  45963  dfac5prim  46022  modelac8prim  46024  permac8prim  46046  ndisj2  46110  limsupre2lem  46776  cncfiooicclem1  46945  iblcncfioo  47030  stoweidlem28  47080  sge0iunmpt  47470  chnerlem1  47934  n0nsn2el  48137  afvfv0bi  48264  2ffzoeq  48440  m1modmmod  48476  modm1p1ne  48488  iccpartiltu  48546  iccpartlt  48548  icceuelpartlem  48559  lighneallem4  48737  oddprmALTV  48827  evenprm2  48854  odd2prm2  48858  even3prm2  48859  upgrimpthslem2  49048  gpg5nbgrvtx03starlem1  49208  gpg5nbgrvtx03starlem2  49209  gpg5nbgrvtx03starlem3  49210  gpg5nbgrvtx13starlem1  49211  gpg5nbgrvtx13starlem2  49212  gpg5nbgrvtx13starlem3  49213  pg4cyclnex  49267  gpg5edgnedg  49270  upgrwlkupwlk  49280  copisnmnd  49308  pgrpgt2nabl  49520  islindeps  49607  lincext1  49608  lindslinindsimp2lem5  49616  snlindsntor  49625  ldepslinc  49663  rrx2linest  49896  line2ylem  49905  line2xlem  49907  oppcmndclem  50167