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  3211  dfpss2  4047  dfdif3OLD  4077  n0f  4308  n0  4312  abn0  4344  2nreu  4403  raaan2  4480  ifnefalse  4496  snnzb  4678  raldifsni  4755  eqsn  4789  n0snor2el  4793  opthpr  4811  prneimg2  4815  opthprneg  4825  unissint  4932  iununi  5058  disji2  5086  opthneg  5436  otthne  5441  opab0  5509  xpcan  6137  xpcan2  6138  xpima  6143  unixpid  6245  unizlim  6445  dff14a  7227  orduniorsuc  7785  dflim3  7803  tfindsg  7817  nn0suc  7850  findsg  7853  resf1extb  7890  xpord2pred  8101  xpord2indlem  8103  frxp3  8107  suppvalbr  8120  frrlem14  8255  tz7.49  8390  oevn0  8456  fsetexb  8814  php  9148  1sdom  9171  1sdomOLD  9172  fimaxg  9210  fiint  9253  fiintOLD  9254  wemapsolem  9479  card2on  9483  brwdomn0  9498  rankxplim2  9809  rankxplim3  9810  updjudhf  9860  carden2a  9895  enpr2  9931  dfackm  10096  fin1a2lem12  10340  ac6num  10408  zorn2lem4  10428  zorn2lem7  10431  brdom3  10457  iundom2g  10469  r1tskina  10711  ltlen  11251  uzm1  12807  xrnemnf  13053  xrnepnf  13054  ioo0  13307  ico0  13328  ioc0  13329  icc0  13330  fzne1  13541  elfznelfzo  13709  elfznelfzob  13710  injresinjlem  13724  fleqceilz  13792  fsuppmapnn0fiubex  13933  sq01  14166  hash1snb  14360  hashgt12el  14363  hashgt12el2  14364  hashfun  14378  hash2prde  14411  hashge2el2dif  14421  fundmge2nop0  14443  repswcshw  14753  cshw1  14763  incexc2  15780  sqrt2irr  16193  divalglem8  16346  ndvdssub  16355  algcvgblem  16523  lcmcllem  16542  lcmfunsnlem2  16586  isprm3  16629  isprm4  16630  2mulprm  16639  ramcl2lem  16956  cshwshashlem1  17042  cshwshash  17051  smndex2dnrinv  18818  sgrp2nmndlem3  18828  sgrp2nmndlem5  18832  symg2bas  19299  odfval  19438  dprdfeq0  19930  isnirred  20305  isirred2  20306  isnzr2  20403  isdomn5  20595  isdomn2OLD  20597  isdomn3  20600  drngmul0orOLD  20646  drngmuleq0  20648  sdrgacs  20686  lvecvs0or  20994  lvecvscan  20997  domnchr  21418  gsummoncoe1  22171  dmatmul  22360  mulmarep1gsum2  22437  mdetunilem8  22482  mp2pm2mplem4  22672  fvmptnn04if  22712  elcls  22936  opnnei  22983  ist0-3  23208  ist1-2  23210  dfconn2  23282  cnconn  23285  pthaus  23501  xkohaus  23516  hausflim  23844  cldsubg  23974  bcth  25205  ioorinv  25453  tdeglem4  25941  fta1b  26053  plydivex  26181  aalioulem3  26218  dvradcnv  26306  cxpcl  26559  recxpcl  26560  logrec  26649  isosctrlem2  26705  efrlim  26855  efrlimOLD  26856  muval2  27020  musum  27077  dchrelbas2  27124  dchrelbas4  27130  dchrfi  27142  dchrptlem3  27153  dchrsum2  27155  sumdchr2  27157  lgscllem  27191  2sqb  27319  2sqcoprm  27322  dchrvmasumiflem2  27389  rpvmasum2  27399  padicabv  27517  padicabvf  27518  padicabvcxp  27519  sltval2  27544  sltres  27550  noseponlem  27552  nosepon  27553  nosepeq  27573  nosupbnd2lem1  27603  noinfbnd2lem1  27618  noetasuplem4  27624  noetainflem4  27628  eln0s  28227  dfnns2  28237  tglowdim1i  28404  tgbtwnconn1  28478  colline  28552  colmid  28591  lmimid  28697  lmiisolem  28699  brbtwn2  28808  colinearalg  28813  axlowdimlem6  28850  axlowdimlem14  28858  axcontlem12  28878  incistruhgr  28982  umgr2edg1  29114  nb3grprlem1  29283  1egrvtxdg0  29415  vtxdginducedm1lem4  29446  wlkdlem4  29587  lfgriswlk  29590  pthdlem2  29671  wwlksnext  29796  clwwlknclwwlkdif  29881  clwlkclwwlklem2a4  29899  clwwisshclwwsn  29918  1wlkdlem4  30042  eupth2lem1  30120  eupth2lem3lem4  30133  frgr3vlem1  30175  frgr3vlem2  30176  3vfriswmgrlem  30179  4cycl2vnunb  30192  frgrncvvdeqlem8  30208  frgrregorufr  30227  frgrreg  30296  frgrregord013  30297  9p10ne21fool  30373  nvmul0or  30552  nmogtmnf  30672  hvmul0or  30927  hvmulcan  30974  hvmulcan2  30975  hiidge0  31000  bcsiALT  31081  shne0i  31350  nonbooli  31553  nmopgtmnf  31770  unopbd  31917  nmcfnlbi  31954  nmopcoi  31997  chirredi  32296  mdsymlem5  32309  sumdmdlem2  32321  n0nsnel  32417  disji2f  32479  aciunf1  32560  hashxpe  32705  sgn3da  32732  elrgspnlem2  33167  ply1dg3rt0irred  33524  sitgaddlemb  34312  plymulx  34512  bnj1109  34749  bnj1542  34820  bnj1253  34980  dff15  35047  lfuhgr3  35080  dfacycgr1  35104  subfacp1lem6  35145  cvmsdisj  35230  satffunlem1lem1  35362  satffunlem2lem1  35364  satffun  35369  btwnconn1lem13  36060  lineunray  36108  rankeq1o  36132  elicc3  36278  nn0prpw  36284  ordtoplem  36396  bj-snmoore  37074  irrdifflemf  37286  icorempo  37312  matunitlindflem1  37583  poimirlem1  37588  poimirlem14  37601  poimirlem16  37603  poimirlem19  37606  poimirlem23  37610  poimirlem25  37612  poimirlem26  37613  itg2addnclem3  37640  itgaddnclem2  37646  fdc  37712  ismgmOLD  37817  cvrval2  39240  cvrnbtwn2  39241  cvrnbtwn3  39242  cvlsupr3  39310  cvrat4  39410  2at0mat0  39492  dalawlem13  39850  isltrn2N  40087  trlator0  40138  cdleme22b  40308  dochkrshp  41353  dochkrshp4  41356  lcfl6  41467  lclkrlem2x  41497  hashnexinj  42089  rspcsbnea  42092  aks6d1c5  42100  nnn1suc  42227  expeqidd  42286  remullid  42395  fimgmcyc  42495  infdesc  42604  fphpd  42777  jm2.23  42958  dflim6  43226  onsucf1olem  43232  onov0suclim  43236  oenassex  43280  tfsconcatb0  43306  tfsconcat0b  43308  naddwordnexlem4  43363  safesnsupfilb  43380  faosnf0.11b  43389  dfsucon  43485  iunrelexp0  43664  ntrneineine1lem  44046  pm13.196a  44376  onfrALTlem5  44505  onfrALTlem3  44507  en3lpVD  44807  onfrALTlem5VD  44847  onfrALTlem3VD  44849  ax6e2ndeqVD  44871  ax6e2ndeqALT  44893  isosctrlem1ALT  44896  rext0  44901  dfac5prim  44953  modelac8prim  44955  permac8prim  44977  ndisj2  45018  limsupre2lem  45695  cncfiooicclem1  45864  iblcncfioo  45949  stoweidlem28  45999  sge0iunmpt  46389  n0nsn2el  46999  afvfv0bi  47126  2ffzoeq  47301  m1modmmod  47332  modm1p1ne  47344  iccpartiltu  47396  iccpartlt  47398  icceuelpartlem  47409  lighneallem4  47584  oddprmALTV  47661  evenprm2  47688  odd2prm2  47692  even3prm2  47693  upgrimpthslem2  47881  gpg5nbgrvtx03starlem1  48032  gpg5nbgrvtx03starlem2  48033  gpg5nbgrvtx03starlem3  48034  gpg5nbgrvtx13starlem1  48035  gpg5nbgrvtx13starlem2  48036  gpg5nbgrvtx13starlem3  48037  pg4cyclnex  48090  upgrwlkupwlk  48101  copisnmnd  48130  pgrpgt2nabl  48327  islindeps  48415  lincext1  48416  lindslinindsimp2lem5  48424  snlindsntor  48433  ldepslinc  48471  rrx2linest  48704  line2ylem  48713  line2xlem  48715  oppcmndclem  48979