Definition df-ne 2958

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 2957	. 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  2959  neir  2960  nne  2961  neneqd  2962  neqned  2964  eqneqall  2968  necon2bd  2973  necon1bd  2975  necon3d  2978  necon2d  2980  necon1bi  2985  necon1i  2990  necon3abid  2993  necon1bbid  2996  necon3bid  3001  necon3abii  3003  necon3bii  3009  neor  3049  neanior  3050  neorian  3052  nfne  3060  nfned  3061  nabbib  3062  nelb  3240  dfpss2  4041  dfdif3OLD  4072  n0f  4302  n0  4306  abn0  4340  2nreu  4408  raaan2  4482  ifnefalse  4498  snnzb  4683  raldifsni  4762  eqsn  4794  n0snor2el  4797  opthpr  4815  prneimg2  4819  opthprneg  4829  unissint  4936  iununi  5064  disji2  5092  opthneg  5462  otthne  5467  opab0  5538  xpcan  6173  xpcan2  6174  xpima  6179  unixpid  6285  unizlim  6485  dff14a  7268  orduniorsuc  7824  dflim3  7841  tfindsg  7855  nn0suc  7889  findsg  7892  resf1extb  7929  xpord2pred  8139  xpord2indlem  8141  frxp3  8145  suppvalbr  8158  frrlem14  8294  tz7.49  8430  oevn0  8498  fsetexb  8859  php  9189  1sdom  9213  fimaxg  9245  fiint  9284  wemapsolem  9510  card2on  9514  brwdomn0  9529  rankxplim2  9850  rankxplim3  9851  updjudhf  9924  carden2a  9959  enpr2  9995  dfackm  10157  fin1a2lem12  10401  ac6num  10469  zorn2lem4  10489  zorn2lem7  10492  brdom3  10518  iundom2g  10530  r1tskina  10773  ltlen  11317  uzm1  12902  xrnemnf  13148  xrnepnf  13149  ioo0  13403  ico0  13424  ioc0  13425  icc0  13426  fzne1  13639  elfznelfzo  13809  elfznelfzob  13810  injresinjlem  13826  fleqceilz  13894  fsuppmapnn0fiubex  14035  sq01  14268  hash1snb  14463  hashgt12el  14466  hashgt12el2  14467  hashfun  14481  hash2prde  14514  hashge2el2dif  14524  fundmge2nop0  14546  repswcshw  14856  cshw1  14866  sgn3da  15145  incexc2  15899  sqrt2irr  16311  divalglem8  16464  ndvdssub  16473  algcvgblem  16641  lcmcllem  16660  lcmfunsnlem2  16704  isprm3  16747  isprm4  16748  2mulprm  16757  ramcl2lem  17075  cshwshashlem1  17161  cshwshash  17170  smndex2dnrinv  18983  sgrp2nmndlem3  18993  sgrp2nmndlem5  18997  symg2bas  19469  odfval  19608  dprdfeq0  20100  isnirred  20509  isirred2  20510  isnzr2  20626  isdomn5  20820  isdomn3  20824  drngmuleq0  20877  sdrgacs  20915  lvecvs0or  21243  lvecvscan  21246  domnchr  21693  gsummoncoe1  22479  dmatmul  22665  mulmarep1gsum2  22742  mdetunilem8  22787  mp2pm2mplem4  22977  fvmptnn04if  23017  elcls  23241  opnnei  23288  ist0-3  23513  ist1-2  23515  dfconn2  23587  cnconn  23590  pthaus  23806  xkohaus  23821  hausflim  24149  cldsubg  24279  bcth  25499  ioorinv  25746  tdeglem4  26228  fta1b  26340  plymulidp  26454  plydivex  26469  aalioulem3  26508  dvradcnv  26595  cxpcl  26850  recxpcl  26851  logrec  26939  isosctrlem2  26995  efrlim  27145  muval2  27309  musum  27366  dchrelbas2  27412  dchrelbas4  27418  dchrfi  27430  dchrptlem3  27441  dchrsum2  27443  sumdchr2  27445  lgscllem  27479  2sqb  27607  2sqcoprm  27610  dchrvmasumiflem2  27677  rpvmasum2  27687  padicabv  27805  padicabvf  27806  padicabvcxp  27807  ltsval2  27831  ltsres  27837  noseponlem  27839  nosepon  27840  nosepeq  27860  nosupbnd2lem1  27890  noinfbnd2lem1  27905  noetasuplem4  27911  noetainflem4  27915  eln0s  28565  dfnns2  28576  bdayfinbndlem1  28671  tglowdim1i  28781  tgbtwnconn1  28855  colline  28934  colmid  28976  lmimid  29114  lmiisolem  29116  brbtwn2  29266  colinearalg  29271  axlowdimlem6  29308  axlowdimlem14  29316  axcontlem12  29336  incistruhgr  29440  umgr2edg1  29572  nb3grprlem1  29741  1egrvtxdg0  29872  vtxdginducedm1lem4  29903  wlkdlem4  30044  lfgriswlk  30047  pthdlem2  30128  wwlksnext  30253  clwwlknclwwlkdif  30341  clwlkclwwlklem2a4  30359  clwwisshclwwsn  30378  1wlkdlem4  30502  eupth2lem1  30580  eupth2lem3lem4  30593  frgr3vlem1  30635  frgr3vlem2  30636  3vfriswmgrlem  30639  4cycl2vnunb  30652  frgrncvvdeqlem8  30668  frgrregorufr  30687  frgrreg  30756  frgrregord013  30757  9p10ne21fool  30833  nvmul0or  31013  nmogtmnf  31133  hvmul0or  31388  hvmulcan  31435  hvmulcan2  31436  hiidge0  31461  bcsiALT  31542  shne0i  31811  nonbooli  32014  nmopgtmnf  32231  unopbd  32378  nmcfnlbi  32415  nmopcoi  32458  chirredi  32757  mdsymlem5  32770  sumdmdlem2  32782  n0nsnel  32872  disji2f  32933  aciunf1  33019  hashxpe  33163  elrgspnlem2  33572  ply1dg3rt0irred  33883  extdgfialglem1  34091  sitgaddlemb  34747  bnj1109  35184  bnj1542  35254  bnj1253  35414  dff15  35481  lfuhgr3  35620  dfacycgr1  35644  subfacp1lem6  35685  cvmsdisj  35770  satffunlem1lem1  35902  satffunlem2lem1  35904  satffun  35909  btwnconn1lem13  36599  lineunray  36647  rankeq1o  36671  nmulel1  36715  elicc3  36856  nn0prpw  36862  ordtoplem  36974  bj-snmoore  37783  irrdifflemf  37997  qdiffALT  38000  icorempo  38025  matunitlindflem1  38295  poimirlem1  38300  poimirlem14  38313  poimirlem16  38315  poimirlem19  38318  poimirlem23  38322  poimirlem25  38324  poimirlem26  38325  itg2addnclem3  38352  itgaddnclem2  38358  fdc  38424  ismgmOLD  38529  cvrval2  40076  cvrnbtwn2  40077  cvrnbtwn3  40078  cvlsupr3  40146  cvrat4  40245  2at0mat0  40327  dalawlem13  40685  isltrn2N  40922  trlator0  40973  cdleme22b  41143  dochkrshp  42188  dochkrshp4  42191  lcfl6  42302  lclkrlem2x  42332  hashnexinj  42923  rspcsbnea  42926  aks6d1c5  42934  nnn1suc  43061  expeqidd  43114  remullid  43223  fimgmcyc  43330  infdesc  43403  fphpd  43571  jm2.23  43751  dflim6  44019  onsucf1olem  44025  onov0suclim  44029  oenassex  44073  tfsconcatb0  44099  tfsconcat0b  44101  naddwordnexlem4  44156  safesnsupfilb  44172  faosnf0.11b  44181  dfsucon  44277  iunrelexp0  44456  ntrneineine1lem  44838  pm13.196a  45152  onfrALTlem5  45279  onfrALTlem3  45281  en3lpVD  45581  onfrALTlem5VD  45621  onfrALTlem3VD  45623  ax6e2ndeqVD  45645  ax6e2ndeqALT  45667  isosctrlem1ALT  45670  rext0  45675  dfac5prim  45727  modelac8prim  45729  permac8prim  45751  ndisj2  45799  limsupre2lem  46466  cncfiooicclem1  46635  iblcncfioo  46720  stoweidlem28  46770  sge0iunmpt  47160  chnerlem1  47626  n0nsn2el  47790  afvfv0bi  47917  2ffzoeq  48093  m1modmmod  48129  modm1p1ne  48141  iccpartiltu  48199  iccpartlt  48201  icceuelpartlem  48212  lighneallem4  48390  oddprmALTV  48480  evenprm2  48507  odd2prm2  48511  even3prm2  48512  upgrimpthslem2  48701  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  pg4cyclnex  48920  gpg5edgnedg  48923  upgrwlkupwlk  48933  copisnmnd  48962  pgrpgt2nabl  49174  islindeps  49261  lincext1  49262  lindslinindsimp2lem5  49270  snlindsntor  49279  ldepslinc  49317  rrx2linest  49550  line2ylem  49559  line2xlem  49561  oppcmndclem  49823