Definition df-ne 2931

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

This definition is referenced by:  neii  2932  neir  2933  nne  2934  neneqd  2935  neqned  2937  eqneqall  2941  necon2bd  2946  necon1bd  2948  necon3d  2951  necon2d  2953  necon1bi  2958  necon1i  2963  necon3abid  2966  necon1bbid  2969  necon3bid  2974  necon3abii  2976  necon3bii  2982  neor  3022  neanior  3023  neorian  3025  nfne  3031  nfned  3032  nabbib  3033  nelb  3210  dfpss2  4038  dfdif3OLD  4068  n0f  4299  n0  4303  abn0  4335  2nreu  4394  raaan2  4473  ifnefalse  4489  snnzb  4673  raldifsni  4749  eqsn  4783  n0snor2el  4787  opthpr  4805  prneimg2  4809  opthprneg  4819  unissint  4925  iununi  5052  disji2  5080  opthneg  5427  otthne  5432  opab0  5500  xpcan  6132  xpcan2  6133  xpima  6138  unixpid  6240  unizlim  6439  dff14a  7214  orduniorsuc  7770  dflim3  7787  tfindsg  7801  nn0suc  7834  findsg  7837  resf1extb  7874  xpord2pred  8085  xpord2indlem  8087  frxp3  8091  suppvalbr  8104  frrlem14  8239  tz7.49  8374  oevn0  8440  fsetexb  8799  php  9129  1sdom  9153  fimaxg  9185  fiint  9225  wemapsolem  9453  card2on  9457  brwdomn0  9472  rankxplim2  9790  rankxplim3  9791  updjudhf  9841  carden2a  9876  enpr2  9912  dfackm  10075  fin1a2lem12  10319  ac6num  10387  zorn2lem4  10407  zorn2lem7  10410  brdom3  10436  iundom2g  10448  r1tskina  10691  ltlen  11232  uzm1  12783  xrnemnf  13029  xrnepnf  13030  ioo0  13284  ico0  13305  ioc0  13306  icc0  13307  fzne1  13518  elfznelfzo  13687  elfznelfzob  13688  injresinjlem  13704  fleqceilz  13772  fsuppmapnn0fiubex  13913  sq01  14146  hash1snb  14340  hashgt12el  14343  hashgt12el2  14344  hashfun  14358  hash2prde  14391  hashge2el2dif  14401  fundmge2nop0  14423  repswcshw  14733  cshw1  14743  incexc2  15759  sqrt2irr  16172  divalglem8  16325  ndvdssub  16334  algcvgblem  16502  lcmcllem  16521  lcmfunsnlem2  16565  isprm3  16608  isprm4  16609  2mulprm  16618  ramcl2lem  16935  cshwshashlem1  17021  cshwshash  17030  smndex2dnrinv  18838  sgrp2nmndlem3  18848  sgrp2nmndlem5  18852  symg2bas  19320  odfval  19459  dprdfeq0  19951  isnirred  20354  isirred2  20355  isnzr2  20449  isdomn5  20641  isdomn2OLD  20643  isdomn3  20646  drngmul0orOLD  20692  drngmuleq0  20694  sdrgacs  20732  lvecvs0or  21061  lvecvscan  21064  domnchr  21485  gsummoncoe1  22250  dmatmul  22439  mulmarep1gsum2  22516  mdetunilem8  22561  mp2pm2mplem4  22751  fvmptnn04if  22791  elcls  23015  opnnei  23062  ist0-3  23287  ist1-2  23289  dfconn2  23361  cnconn  23364  pthaus  23580  xkohaus  23595  hausflim  23923  cldsubg  24053  bcth  25283  ioorinv  25531  tdeglem4  26019  fta1b  26131  plydivex  26259  aalioulem3  26296  dvradcnv  26384  cxpcl  26637  recxpcl  26638  logrec  26727  isosctrlem2  26783  efrlim  26933  efrlimOLD  26934  muval2  27098  musum  27155  dchrelbas2  27202  dchrelbas4  27208  dchrfi  27220  dchrptlem3  27231  dchrsum2  27233  sumdchr2  27235  lgscllem  27269  2sqb  27397  2sqcoprm  27400  dchrvmasumiflem2  27467  rpvmasum2  27477  padicabv  27595  padicabvf  27596  padicabvcxp  27597  sltval2  27622  sltres  27628  noseponlem  27630  nosepon  27631  nosepeq  27651  nosupbnd2lem1  27681  noinfbnd2lem1  27696  noetasuplem4  27702  noetainflem4  27706  eln0s  28320  dfnns2  28330  tglowdim1i  28522  tgbtwnconn1  28596  colline  28670  colmid  28709  lmimid  28815  lmiisolem  28817  brbtwn2  28927  colinearalg  28932  axlowdimlem6  28969  axlowdimlem14  28977  axcontlem12  28997  incistruhgr  29101  umgr2edg1  29233  nb3grprlem1  29402  1egrvtxdg0  29534  vtxdginducedm1lem4  29565  wlkdlem4  29706  lfgriswlk  29709  pthdlem2  29790  wwlksnext  29915  clwwlknclwwlkdif  30003  clwlkclwwlklem2a4  30021  clwwisshclwwsn  30040  1wlkdlem4  30164  eupth2lem1  30242  eupth2lem3lem4  30255  frgr3vlem1  30297  frgr3vlem2  30298  3vfriswmgrlem  30301  4cycl2vnunb  30314  frgrncvvdeqlem8  30330  frgrregorufr  30349  frgrreg  30418  frgrregord013  30419  9p10ne21fool  30495  nvmul0or  30674  nmogtmnf  30794  hvmul0or  31049  hvmulcan  31096  hvmulcan2  31097  hiidge0  31122  bcsiALT  31203  shne0i  31472  nonbooli  31675  nmopgtmnf  31892  unopbd  32039  nmcfnlbi  32076  nmopcoi  32119  chirredi  32418  mdsymlem5  32431  sumdmdlem2  32443  n0nsnel  32539  disji2f  32601  aciunf1  32690  hashxpe  32836  sgn3da  32864  elrgspnlem2  33274  ply1dg3rt0irred  33614  extdgfialglem1  33798  sitgaddlemb  34454  plymulx  34654  bnj1109  34891  bnj1542  34962  bnj1253  35122  dff15  35189  lfuhgr3  35263  dfacycgr1  35287  subfacp1lem6  35328  cvmsdisj  35413  satffunlem1lem1  35545  satffunlem2lem1  35547  satffun  35552  btwnconn1lem13  36242  lineunray  36290  rankeq1o  36314  elicc3  36460  nn0prpw  36466  ordtoplem  36578  bj-snmoore  37257  irrdifflemf  37469  icorempo  37495  matunitlindflem1  37756  poimirlem1  37761  poimirlem14  37774  poimirlem16  37776  poimirlem19  37779  poimirlem23  37783  poimirlem25  37785  poimirlem26  37786  itg2addnclem3  37813  itgaddnclem2  37819  fdc  37885  ismgmOLD  37990  cvrval2  39473  cvrnbtwn2  39474  cvrnbtwn3  39475  cvlsupr3  39543  cvrat4  39642  2at0mat0  39724  dalawlem13  40082  isltrn2N  40319  trlator0  40370  cdleme22b  40540  dochkrshp  41585  dochkrshp4  41588  lcfl6  41699  lclkrlem2x  41729  hashnexinj  42321  rspcsbnea  42324  aks6d1c5  42332  nnn1suc  42463  expeqidd  42522  remullid  42631  fimgmcyc  42731  infdesc  42828  fphpd  43000  jm2.23  43180  dflim6  43448  onsucf1olem  43454  onov0suclim  43458  oenassex  43502  tfsconcatb0  43528  tfsconcat0b  43530  naddwordnexlem4  43585  safesnsupfilb  43601  faosnf0.11b  43610  dfsucon  43706  iunrelexp0  43885  ntrneineine1lem  44267  pm13.196a  44597  onfrALTlem5  44725  onfrALTlem3  44727  en3lpVD  45027  onfrALTlem5VD  45067  onfrALTlem3VD  45069  ax6e2ndeqVD  45091  ax6e2ndeqALT  45113  isosctrlem1ALT  45116  rext0  45121  dfac5prim  45173  modelac8prim  45175  permac8prim  45197  ndisj2  45238  limsupre2lem  45910  cncfiooicclem1  46079  iblcncfioo  46164  stoweidlem28  46214  sge0iunmpt  46604  chnerlem1  47068  n0nsn2el  47213  afvfv0bi  47340  2ffzoeq  47515  m1modmmod  47546  modm1p1ne  47558  iccpartiltu  47610  iccpartlt  47612  icceuelpartlem  47623  lighneallem4  47798  oddprmALTV  47875  evenprm2  47902  odd2prm2  47906  even3prm2  47907  upgrimpthslem2  48096  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem2  48260  gpg5nbgrvtx13starlem3  48261  pg4cyclnex  48315  gpg5edgnedg  48318  upgrwlkupwlk  48328  copisnmnd  48357  pgrpgt2nabl  48554  islindeps  48641  lincext1  48642  lindslinindsimp2lem5  48650  snlindsntor  48659  ldepslinc  48697  rrx2linest  48930  line2ylem  48939  line2xlem  48941  oppcmndclem  49204