Definition df-ne 2926

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

This definition is referenced by:  neii  2927  neir  2928  nne  2929  neneqd  2930  neqned  2932  eqneqall  2936  necon2bd  2941  necon1bd  2943  necon3d  2946  necon2d  2948  necon1bi  2953  necon1i  2958  necon3abid  2961  necon1bbid  2964  necon3bid  2969  necon3abii  2971  necon3bii  2977  neor  3017  neanior  3018  neorian  3020  nfne  3026  nfned  3027  nabbib  3028  nelb  3213  dfpss2  4051  dfdif3OLD  4081  n0f  4312  n0  4316  abn0  4348  2nreu  4407  raaan2  4484  ifnefalse  4500  snnzb  4682  raldifsni  4759  eqsn  4793  n0snor2el  4797  opthpr  4815  prneimg2  4819  opthprneg  4829  unissint  4936  iununi  5063  disji2  5091  opthneg  5441  otthne  5446  opab0  5514  xpcan  6149  xpcan2  6150  xpima  6155  unixpid  6257  unizlim  6457  dff14a  7245  orduniorsuc  7805  dflim3  7823  tfindsg  7837  nn0suc  7870  findsg  7873  resf1extb  7910  xpord2pred  8124  xpord2indlem  8126  frxp3  8130  suppvalbr  8143  frrlem14  8278  tz7.49  8413  oevn0  8479  fsetexb  8837  php  9171  1sdom  9195  1sdomOLD  9196  fimaxg  9234  fiint  9277  fiintOLD  9278  wemapsolem  9503  card2on  9507  brwdomn0  9522  rankxplim2  9833  rankxplim3  9834  updjudhf  9884  carden2a  9919  enpr2  9955  dfackm  10120  fin1a2lem12  10364  ac6num  10432  zorn2lem4  10452  zorn2lem7  10455  brdom3  10481  iundom2g  10493  r1tskina  10735  ltlen  11275  uzm1  12831  xrnemnf  13077  xrnepnf  13078  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  fzne1  13565  elfznelfzo  13733  elfznelfzob  13734  injresinjlem  13748  fleqceilz  13816  fsuppmapnn0fiubex  13957  sq01  14190  hash1snb  14384  hashgt12el  14387  hashgt12el2  14388  hashfun  14402  hash2prde  14435  hashge2el2dif  14445  fundmge2nop0  14467  repswcshw  14777  cshw1  14787  incexc2  15804  sqrt2irr  16217  divalglem8  16370  ndvdssub  16379  algcvgblem  16547  lcmcllem  16566  lcmfunsnlem2  16610  isprm3  16653  isprm4  16654  2mulprm  16663  ramcl2lem  16980  cshwshashlem1  17066  cshwshash  17075  smndex2dnrinv  18842  sgrp2nmndlem3  18852  sgrp2nmndlem5  18856  symg2bas  19323  odfval  19462  dprdfeq0  19954  isnirred  20329  isirred2  20330  isnzr2  20427  isdomn5  20619  isdomn2OLD  20621  isdomn3  20624  drngmul0orOLD  20670  drngmuleq0  20672  sdrgacs  20710  lvecvs0or  21018  lvecvscan  21021  domnchr  21442  gsummoncoe1  22195  dmatmul  22384  mulmarep1gsum2  22461  mdetunilem8  22506  mp2pm2mplem4  22696  fvmptnn04if  22736  elcls  22960  opnnei  23007  ist0-3  23232  ist1-2  23234  dfconn2  23306  cnconn  23309  pthaus  23525  xkohaus  23540  hausflim  23868  cldsubg  23998  bcth  25229  ioorinv  25477  tdeglem4  25965  fta1b  26077  plydivex  26205  aalioulem3  26242  dvradcnv  26330  cxpcl  26583  recxpcl  26584  logrec  26673  isosctrlem2  26729  efrlim  26879  efrlimOLD  26880  muval2  27044  musum  27101  dchrelbas2  27148  dchrelbas4  27154  dchrfi  27166  dchrptlem3  27177  dchrsum2  27179  sumdchr2  27181  lgscllem  27215  2sqb  27343  2sqcoprm  27346  dchrvmasumiflem2  27413  rpvmasum2  27423  padicabv  27541  padicabvf  27542  padicabvcxp  27543  sltval2  27568  sltres  27574  noseponlem  27576  nosepon  27577  nosepeq  27597  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetasuplem4  27648  noetainflem4  27652  eln0s  28251  dfnns2  28261  tglowdim1i  28428  tgbtwnconn1  28502  colline  28576  colmid  28615  lmimid  28721  lmiisolem  28723  brbtwn2  28832  colinearalg  28837  axlowdimlem6  28874  axlowdimlem14  28882  axcontlem12  28902  incistruhgr  29006  umgr2edg1  29138  nb3grprlem1  29307  1egrvtxdg0  29439  vtxdginducedm1lem4  29470  wlkdlem4  29613  lfgriswlk  29616  pthdlem2  29698  wwlksnext  29823  clwwlknclwwlkdif  29908  clwlkclwwlklem2a4  29926  clwwisshclwwsn  29945  1wlkdlem4  30069  eupth2lem1  30147  eupth2lem3lem4  30160  frgr3vlem1  30202  frgr3vlem2  30203  3vfriswmgrlem  30206  4cycl2vnunb  30219  frgrncvvdeqlem8  30235  frgrregorufr  30254  frgrreg  30323  frgrregord013  30324  9p10ne21fool  30400  nvmul0or  30579  nmogtmnf  30699  hvmul0or  30954  hvmulcan  31001  hvmulcan2  31002  hiidge0  31027  bcsiALT  31108  shne0i  31377  nonbooli  31580  nmopgtmnf  31797  unopbd  31944  nmcfnlbi  31981  nmopcoi  32024  chirredi  32323  mdsymlem5  32336  sumdmdlem2  32348  n0nsnel  32444  disji2f  32506  aciunf1  32587  hashxpe  32732  sgn3da  32759  elrgspnlem2  33194  ply1dg3rt0irred  33551  sitgaddlemb  34339  plymulx  34539  bnj1109  34776  bnj1542  34847  bnj1253  35007  dff15  35074  lfuhgr3  35107  dfacycgr1  35131  subfacp1lem6  35172  cvmsdisj  35257  satffunlem1lem1  35389  satffunlem2lem1  35391  satffun  35396  btwnconn1lem13  36087  lineunray  36135  rankeq1o  36159  elicc3  36305  nn0prpw  36311  ordtoplem  36423  bj-snmoore  37101  irrdifflemf  37313  icorempo  37339  matunitlindflem1  37610  poimirlem1  37615  poimirlem14  37628  poimirlem16  37630  poimirlem19  37633  poimirlem23  37637  poimirlem25  37639  poimirlem26  37640  itg2addnclem3  37667  itgaddnclem2  37673  fdc  37739  ismgmOLD  37844  cvrval2  39267  cvrnbtwn2  39268  cvrnbtwn3  39269  cvlsupr3  39337  cvrat4  39437  2at0mat0  39519  dalawlem13  39877  isltrn2N  40114  trlator0  40165  cdleme22b  40335  dochkrshp  41380  dochkrshp4  41383  lcfl6  41494  lclkrlem2x  41524  hashnexinj  42116  rspcsbnea  42119  aks6d1c5  42127  nnn1suc  42254  expeqidd  42313  remullid  42422  fimgmcyc  42522  infdesc  42631  fphpd  42804  jm2.23  42985  dflim6  43253  onsucf1olem  43259  onov0suclim  43263  oenassex  43307  tfsconcatb0  43333  tfsconcat0b  43335  naddwordnexlem4  43390  safesnsupfilb  43407  faosnf0.11b  43416  dfsucon  43512  iunrelexp0  43691  ntrneineine1lem  44073  pm13.196a  44403  onfrALTlem5  44532  onfrALTlem3  44534  en3lpVD  44834  onfrALTlem5VD  44874  onfrALTlem3VD  44876  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  isosctrlem1ALT  44923  rext0  44928  dfac5prim  44980  modelac8prim  44982  permac8prim  45004  ndisj2  45045  limsupre2lem  45722  cncfiooicclem1  45891  iblcncfioo  45976  stoweidlem28  46026  sge0iunmpt  46416  n0nsn2el  47023  afvfv0bi  47150  2ffzoeq  47325  m1modmmod  47356  modm1p1ne  47368  iccpartiltu  47420  iccpartlt  47422  icceuelpartlem  47433  lighneallem4  47608  oddprmALTV  47685  evenprm2  47712  odd2prm2  47716  even3prm2  47717  upgrimpthslem2  47905  gpg5nbgrvtx03starlem1  48056  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem2  48060  gpg5nbgrvtx13starlem3  48061  pg4cyclnex  48114  upgrwlkupwlk  48125  copisnmnd  48154  pgrpgt2nabl  48351  islindeps  48439  lincext1  48440  lindslinindsimp2lem5  48448  snlindsntor  48457  ldepslinc  48495  rrx2linest  48728  line2ylem  48737  line2xlem  48739  oppcmndclem  49003