Definition df-ne 2929

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 2928	. 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  2930  neir  2931  nne  2932  neneqd  2933  neqned  2935  eqneqall  2939  necon2bd  2944  necon1bd  2946  necon3d  2949  necon2d  2951  necon1bi  2956  necon1i  2961  necon3abid  2964  necon1bbid  2967  necon3bid  2972  necon3abii  2974  necon3bii  2980  neor  3020  neanior  3021  neorian  3023  nfne  3029  nfned  3030  nabbib  3031  nelb  3208  dfpss2  4035  dfdif3OLD  4065  n0f  4296  n0  4300  abn0  4332  2nreu  4391  raaan2  4468  ifnefalse  4484  snnzb  4668  raldifsni  4744  eqsn  4778  n0snor2el  4782  opthpr  4800  prneimg2  4804  opthprneg  4814  unissint  4920  iununi  5045  disji2  5073  opthneg  5419  otthne  5424  opab0  5492  xpcan  6123  xpcan2  6124  xpima  6129  unixpid  6231  unizlim  6430  dff14a  7204  orduniorsuc  7760  dflim3  7777  tfindsg  7791  nn0suc  7824  findsg  7827  resf1extb  7864  xpord2pred  8075  xpord2indlem  8077  frxp3  8081  suppvalbr  8094  frrlem14  8229  tz7.49  8364  oevn0  8430  fsetexb  8788  php  9116  1sdom  9139  fimaxg  9171  fiint  9211  wemapsolem  9436  card2on  9440  brwdomn0  9455  rankxplim2  9773  rankxplim3  9774  updjudhf  9824  carden2a  9859  enpr2  9895  dfackm  10058  fin1a2lem12  10302  ac6num  10370  zorn2lem4  10390  zorn2lem7  10393  brdom3  10419  iundom2g  10431  r1tskina  10673  ltlen  11214  uzm1  12770  xrnemnf  13016  xrnepnf  13017  ioo0  13270  ico0  13291  ioc0  13292  icc0  13293  fzne1  13504  elfznelfzo  13673  elfznelfzob  13674  injresinjlem  13690  fleqceilz  13758  fsuppmapnn0fiubex  13899  sq01  14132  hash1snb  14326  hashgt12el  14329  hashgt12el2  14330  hashfun  14344  hash2prde  14377  hashge2el2dif  14387  fundmge2nop0  14409  repswcshw  14719  cshw1  14729  incexc2  15745  sqrt2irr  16158  divalglem8  16311  ndvdssub  16320  algcvgblem  16488  lcmcllem  16507  lcmfunsnlem2  16551  isprm3  16594  isprm4  16595  2mulprm  16604  ramcl2lem  16921  cshwshashlem1  17007  cshwshash  17016  smndex2dnrinv  18823  sgrp2nmndlem3  18833  sgrp2nmndlem5  18837  symg2bas  19305  odfval  19444  dprdfeq0  19936  isnirred  20338  isirred2  20339  isnzr2  20433  isdomn5  20625  isdomn2OLD  20627  isdomn3  20630  drngmul0orOLD  20676  drngmuleq0  20678  sdrgacs  20716  lvecvs0or  21045  lvecvscan  21048  domnchr  21469  gsummoncoe1  22223  dmatmul  22412  mulmarep1gsum2  22489  mdetunilem8  22534  mp2pm2mplem4  22724  fvmptnn04if  22764  elcls  22988  opnnei  23035  ist0-3  23260  ist1-2  23262  dfconn2  23334  cnconn  23337  pthaus  23553  xkohaus  23568  hausflim  23896  cldsubg  24026  bcth  25256  ioorinv  25504  tdeglem4  25992  fta1b  26104  plydivex  26232  aalioulem3  26269  dvradcnv  26357  cxpcl  26610  recxpcl  26611  logrec  26700  isosctrlem2  26756  efrlim  26906  efrlimOLD  26907  muval2  27071  musum  27128  dchrelbas2  27175  dchrelbas4  27181  dchrfi  27193  dchrptlem3  27204  dchrsum2  27206  sumdchr2  27208  lgscllem  27242  2sqb  27370  2sqcoprm  27373  dchrvmasumiflem2  27440  rpvmasum2  27450  padicabv  27568  padicabvf  27569  padicabvcxp  27570  sltval2  27595  sltres  27601  noseponlem  27603  nosepon  27604  nosepeq  27624  nosupbnd2lem1  27654  noinfbnd2lem1  27669  noetasuplem4  27675  noetainflem4  27679  eln0s  28287  dfnns2  28297  tglowdim1i  28479  tgbtwnconn1  28553  colline  28627  colmid  28666  lmimid  28772  lmiisolem  28774  brbtwn2  28883  colinearalg  28888  axlowdimlem6  28925  axlowdimlem14  28933  axcontlem12  28953  incistruhgr  29057  umgr2edg1  29189  nb3grprlem1  29358  1egrvtxdg0  29490  vtxdginducedm1lem4  29521  wlkdlem4  29662  lfgriswlk  29665  pthdlem2  29746  wwlksnext  29871  clwwlknclwwlkdif  29959  clwlkclwwlklem2a4  29977  clwwisshclwwsn  29996  1wlkdlem4  30120  eupth2lem1  30198  eupth2lem3lem4  30211  frgr3vlem1  30253  frgr3vlem2  30254  3vfriswmgrlem  30257  4cycl2vnunb  30270  frgrncvvdeqlem8  30286  frgrregorufr  30305  frgrreg  30374  frgrregord013  30375  9p10ne21fool  30451  nvmul0or  30630  nmogtmnf  30750  hvmul0or  31005  hvmulcan  31052  hvmulcan2  31053  hiidge0  31078  bcsiALT  31159  shne0i  31428  nonbooli  31631  nmopgtmnf  31848  unopbd  31995  nmcfnlbi  32032  nmopcoi  32075  chirredi  32374  mdsymlem5  32387  sumdmdlem2  32399  n0nsnel  32495  disji2f  32557  aciunf1  32645  hashxpe  32789  sgn3da  32817  elrgspnlem2  33210  ply1dg3rt0irred  33546  extdgfialglem1  33705  sitgaddlemb  34361  plymulx  34561  bnj1109  34798  bnj1542  34869  bnj1253  35029  dff15  35096  lfuhgr3  35164  dfacycgr1  35188  subfacp1lem6  35229  cvmsdisj  35314  satffunlem1lem1  35446  satffunlem2lem1  35448  satffun  35453  btwnconn1lem13  36143  lineunray  36191  rankeq1o  36215  elicc3  36361  nn0prpw  36367  ordtoplem  36479  bj-snmoore  37157  irrdifflemf  37369  icorempo  37395  matunitlindflem1  37666  poimirlem1  37671  poimirlem14  37684  poimirlem16  37686  poimirlem19  37689  poimirlem23  37693  poimirlem25  37695  poimirlem26  37696  itg2addnclem3  37723  itgaddnclem2  37729  fdc  37795  ismgmOLD  37900  cvrval2  39383  cvrnbtwn2  39384  cvrnbtwn3  39385  cvlsupr3  39453  cvrat4  39552  2at0mat0  39634  dalawlem13  39992  isltrn2N  40229  trlator0  40280  cdleme22b  40450  dochkrshp  41495  dochkrshp4  41498  lcfl6  41609  lclkrlem2x  41639  hashnexinj  42231  rspcsbnea  42234  aks6d1c5  42242  nnn1suc  42369  expeqidd  42428  remullid  42537  fimgmcyc  42637  infdesc  42746  fphpd  42919  jm2.23  43099  dflim6  43367  onsucf1olem  43373  onov0suclim  43377  oenassex  43421  tfsconcatb0  43447  tfsconcat0b  43449  naddwordnexlem4  43504  safesnsupfilb  43521  faosnf0.11b  43530  dfsucon  43626  iunrelexp0  43805  ntrneineine1lem  44187  pm13.196a  44517  onfrALTlem5  44645  onfrALTlem3  44647  en3lpVD  44947  onfrALTlem5VD  44987  onfrALTlem3VD  44989  ax6e2ndeqVD  45011  ax6e2ndeqALT  45033  isosctrlem1ALT  45036  rext0  45041  dfac5prim  45093  modelac8prim  45095  permac8prim  45117  ndisj2  45158  limsupre2lem  45832  cncfiooicclem1  46001  iblcncfioo  46086  stoweidlem28  46136  sge0iunmpt  46526  chnerlem1  46990  n0nsn2el  47135  afvfv0bi  47262  2ffzoeq  47437  m1modmmod  47468  modm1p1ne  47480  iccpartiltu  47532  iccpartlt  47534  icceuelpartlem  47545  lighneallem4  47720  oddprmALTV  47797  evenprm2  47824  odd2prm2  47828  even3prm2  47829  upgrimpthslem2  48018  gpg5nbgrvtx03starlem1  48178  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx03starlem3  48180  gpg5nbgrvtx13starlem1  48181  gpg5nbgrvtx13starlem2  48182  gpg5nbgrvtx13starlem3  48183  pg4cyclnex  48237  gpg5edgnedg  48240  upgrwlkupwlk  48250  copisnmnd  48279  pgrpgt2nabl  48476  islindeps  48564  lincext1  48565  lindslinindsimp2lem5  48573  snlindsntor  48582  ldepslinc  48620  rrx2linest  48853  line2ylem  48862  line2xlem  48864  oppcmndclem  49128