Definition df-ne 2934

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

This definition is referenced by:  neii  2935  neir  2936  nne  2937  neneqd  2938  neqned  2940  eqneqall  2944  necon2bd  2949  necon1bd  2951  necon3d  2954  necon2d  2956  necon1bi  2961  necon1i  2966  necon3abid  2969  necon1bbid  2972  necon3bid  2977  necon3abii  2979  necon3bii  2985  neor  3025  neanior  3026  neorian  3028  nfne  3034  nfned  3035  nabbib  3036  nelb  3214  dfpss2  4042  dfdif3OLD  4072  n0f  4303  n0  4307  abn0  4339  2nreu  4398  raaan2  4477  ifnefalse  4493  snnzb  4677  raldifsni  4753  eqsn  4787  n0snor2el  4791  opthpr  4809  prneimg2  4813  opthprneg  4823  unissint  4929  iununi  5056  disji2  5084  opthneg  5439  otthne  5444  opab0  5512  xpcan  6144  xpcan2  6145  xpima  6150  unixpid  6252  unizlim  6451  dff14a  7228  orduniorsuc  7784  dflim3  7801  tfindsg  7815  nn0suc  7848  findsg  7851  resf1extb  7888  xpord2pred  8099  xpord2indlem  8101  frxp3  8105  suppvalbr  8118  frrlem14  8253  tz7.49  8388  oevn0  8454  fsetexb  8815  php  9145  1sdom  9169  fimaxg  9201  fiint  9241  wemapsolem  9469  card2on  9473  brwdomn0  9488  rankxplim2  9806  rankxplim3  9807  updjudhf  9857  carden2a  9892  enpr2  9928  dfackm  10091  fin1a2lem12  10335  ac6num  10403  zorn2lem4  10423  zorn2lem7  10426  brdom3  10452  iundom2g  10464  r1tskina  10707  ltlen  11248  uzm1  12799  xrnemnf  13045  xrnepnf  13046  ioo0  13300  ico0  13321  ioc0  13322  icc0  13323  fzne1  13534  elfznelfzo  13703  elfznelfzob  13704  injresinjlem  13720  fleqceilz  13788  fsuppmapnn0fiubex  13929  sq01  14162  hash1snb  14356  hashgt12el  14359  hashgt12el2  14360  hashfun  14374  hash2prde  14407  hashge2el2dif  14417  fundmge2nop0  14439  repswcshw  14749  cshw1  14759  incexc2  15775  sqrt2irr  16188  divalglem8  16341  ndvdssub  16350  algcvgblem  16518  lcmcllem  16537  lcmfunsnlem2  16581  isprm3  16624  isprm4  16625  2mulprm  16634  ramcl2lem  16951  cshwshashlem1  17037  cshwshash  17046  smndex2dnrinv  18857  sgrp2nmndlem3  18867  sgrp2nmndlem5  18871  symg2bas  19339  odfval  19478  dprdfeq0  19970  isnirred  20373  isirred2  20374  isnzr2  20468  isdomn5  20660  isdomn2OLD  20662  isdomn3  20665  drngmul0orOLD  20711  drngmuleq0  20713  sdrgacs  20751  lvecvs0or  21080  lvecvscan  21083  domnchr  21504  gsummoncoe1  22269  dmatmul  22458  mulmarep1gsum2  22535  mdetunilem8  22580  mp2pm2mplem4  22770  fvmptnn04if  22810  elcls  23034  opnnei  23081  ist0-3  23306  ist1-2  23308  dfconn2  23380  cnconn  23383  pthaus  23599  xkohaus  23614  hausflim  23942  cldsubg  24072  bcth  25302  ioorinv  25550  tdeglem4  26038  fta1b  26150  plydivex  26278  aalioulem3  26315  dvradcnv  26403  cxpcl  26656  recxpcl  26657  logrec  26746  isosctrlem2  26802  efrlim  26952  efrlimOLD  26953  muval2  27117  musum  27174  dchrelbas2  27221  dchrelbas4  27227  dchrfi  27239  dchrptlem3  27250  dchrsum2  27252  sumdchr2  27254  lgscllem  27288  2sqb  27416  2sqcoprm  27419  dchrvmasumiflem2  27486  rpvmasum2  27496  padicabv  27614  padicabvf  27615  padicabvcxp  27616  ltsval2  27641  ltsres  27647  noseponlem  27649  nosepon  27650  nosepeq  27670  nosupbnd2lem1  27700  noinfbnd2lem1  27715  noetasuplem4  27721  noetainflem4  27725  eln0s  28374  dfnns2  28385  bdayfinbndlem1  28480  tglowdim1i  28591  tgbtwnconn1  28665  colline  28739  colmid  28778  lmimid  28884  lmiisolem  28886  brbtwn2  28996  colinearalg  29001  axlowdimlem6  29038  axlowdimlem14  29046  axcontlem12  29066  incistruhgr  29170  umgr2edg1  29302  nb3grprlem1  29471  1egrvtxdg0  29603  vtxdginducedm1lem4  29634  wlkdlem4  29775  lfgriswlk  29778  pthdlem2  29859  wwlksnext  29984  clwwlknclwwlkdif  30072  clwlkclwwlklem2a4  30090  clwwisshclwwsn  30109  1wlkdlem4  30233  eupth2lem1  30311  eupth2lem3lem4  30324  frgr3vlem1  30366  frgr3vlem2  30367  3vfriswmgrlem  30370  4cycl2vnunb  30383  frgrncvvdeqlem8  30399  frgrregorufr  30418  frgrreg  30487  frgrregord013  30488  9p10ne21fool  30564  nvmul0or  30744  nmogtmnf  30864  hvmul0or  31119  hvmulcan  31166  hvmulcan2  31167  hiidge0  31192  bcsiALT  31273  shne0i  31542  nonbooli  31745  nmopgtmnf  31962  unopbd  32109  nmcfnlbi  32146  nmopcoi  32189  chirredi  32488  mdsymlem5  32501  sumdmdlem2  32513  n0nsnel  32608  disji2f  32670  aciunf1  32759  hashxpe  32904  sgn3da  32932  elrgspnlem2  33343  ply1dg3rt0irred  33683  extdgfialglem1  33876  sitgaddlemb  34532  plymulx  34732  bnj1109  34969  bnj1542  35039  bnj1253  35199  dff15  35267  lfuhgr3  35342  dfacycgr1  35366  subfacp1lem6  35407  cvmsdisj  35492  satffunlem1lem1  35624  satffunlem2lem1  35626  satffun  35631  btwnconn1lem13  36321  lineunray  36369  rankeq1o  36393  elicc3  36539  nn0prpw  36545  ordtoplem  36657  bj-snmoore  37393  irrdifflemf  37607  icorempo  37633  matunitlindflem1  37896  poimirlem1  37901  poimirlem14  37914  poimirlem16  37916  poimirlem19  37919  poimirlem23  37923  poimirlem25  37925  poimirlem26  37926  itg2addnclem3  37953  itgaddnclem2  37959  fdc  38025  ismgmOLD  38130  cvrval2  39679  cvrnbtwn2  39680  cvrnbtwn3  39681  cvlsupr3  39749  cvrat4  39848  2at0mat0  39930  dalawlem13  40288  isltrn2N  40525  trlator0  40576  cdleme22b  40746  dochkrshp  41791  dochkrshp4  41794  lcfl6  41905  lclkrlem2x  41935  hashnexinj  42527  rspcsbnea  42530  aks6d1c5  42538  nnn1suc  42665  expeqidd  42724  remullid  42833  fimgmcyc  42933  infdesc  43030  fphpd  43202  jm2.23  43382  dflim6  43650  onsucf1olem  43656  onov0suclim  43660  oenassex  43704  tfsconcatb0  43730  tfsconcat0b  43732  naddwordnexlem4  43787  safesnsupfilb  43803  faosnf0.11b  43812  dfsucon  43908  iunrelexp0  44087  ntrneineine1lem  44469  pm13.196a  44799  onfrALTlem5  44927  onfrALTlem3  44929  en3lpVD  45229  onfrALTlem5VD  45269  onfrALTlem3VD  45271  ax6e2ndeqVD  45293  ax6e2ndeqALT  45315  isosctrlem1ALT  45318  rext0  45323  dfac5prim  45375  modelac8prim  45377  permac8prim  45399  ndisj2  45440  limsupre2lem  46111  cncfiooicclem1  46280  iblcncfioo  46365  stoweidlem28  46415  sge0iunmpt  46805  chnerlem1  47269  n0nsn2el  47414  afvfv0bi  47541  2ffzoeq  47716  m1modmmod  47747  modm1p1ne  47759  iccpartiltu  47811  iccpartlt  47813  icceuelpartlem  47824  lighneallem4  47999  oddprmALTV  48076  evenprm2  48103  odd2prm2  48107  even3prm2  48108  upgrimpthslem2  48297  gpg5nbgrvtx03starlem1  48457  gpg5nbgrvtx03starlem2  48458  gpg5nbgrvtx03starlem3  48459  gpg5nbgrvtx13starlem1  48460  gpg5nbgrvtx13starlem2  48461  gpg5nbgrvtx13starlem3  48462  pg4cyclnex  48516  gpg5edgnedg  48519  upgrwlkupwlk  48529  copisnmnd  48558  pgrpgt2nabl  48755  islindeps  48842  lincext1  48843  lindslinindsimp2lem5  48851  snlindsntor  48860  ldepslinc  48898  rrx2linest  49131  line2ylem  49140  line2xlem  49142  oppcmndclem  49405