Definition df-ne 2938

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

This definition is referenced by:  neii  2939  neir  2940  nne  2941  neneqd  2942  neqned  2944  eqneqall  2948  necon2bd  2953  necon1bd  2955  necon3d  2958  necon2d  2960  necon1bi  2966  necon1i  2971  necon3abid  2974  necon1bbid  2977  necon3bid  2982  necon3abii  2984  necon3bii  2990  neor  3031  neanior  3032  neorian  3034  nfne  3040  nfned  3041  nabbib  3042  nelb  3231  nelbOLD  3232  dfpss2  4097  dfdif3OLD  4127  n0f  4354  n0  4358  abn0  4390  2nreu  4449  raaan2  4526  ifnefalse  4542  snnzb  4722  raldifsni  4799  eqsn  4833  n0snor2el  4837  opthpr  4855  prneimg2  4859  opthprneg  4869  unissint  4976  iununi  5103  disji2  5131  opthneg  5491  otthne  5496  opab0  5563  xpcan  6197  xpcan2  6198  xpima  6203  unixpid  6305  unizlim  6508  dff14a  7289  orduniorsuc  7849  dflim3  7867  tfindsg  7881  nn0suc  7916  findsg  7919  xpord2pred  8168  xpord2indlem  8170  frxp3  8174  suppvalbr  8187  frrlem14  8322  wfrlem16OLD  8362  tz7.49  8483  oevn0  8551  fsetexb  8902  php  9244  phpOLD  9256  1sdom  9281  1sdomOLD  9282  fimaxg  9320  fiint  9363  fiintOLD  9364  wemapsolem  9587  card2on  9591  brwdomn0  9606  rankxplim2  9917  rankxplim3  9918  updjudhf  9968  carden2a  10003  enpr2  10039  dfackm  10204  fin1a2lem12  10448  ac6num  10516  zorn2lem4  10536  zorn2lem7  10539  brdom3  10565  iundom2g  10577  r1tskina  10819  1re  11258  ltlen  11359  uzm1  12913  xrnemnf  13156  xrnepnf  13157  ioo0  13408  ico0  13429  ioc0  13430  icc0  13431  fzne1  13640  elfznelfzo  13807  elfznelfzob  13808  injresinjlem  13822  fleqceilz  13890  fsuppmapnn0fiubex  14029  sq01  14260  hash1snb  14454  hashgt12el  14457  hashgt12el2  14458  hashfun  14472  hash2prde  14505  hashge2el2dif  14515  fundmge2nop0  14537  repswcshw  14846  cshw1  14856  incexc2  15870  sqrt2irr  16281  divalglem8  16433  ndvdssub  16442  algcvgblem  16610  lcmcllem  16629  lcmfunsnlem2  16673  isprm3  16716  isprm4  16717  2mulprm  16726  ramcl2lem  17042  cshwshashlem1  17129  cshwshash  17138  smndex2dnrinv  18940  sgrp2nmndlem3  18950  sgrp2nmndlem5  18954  symg2bas  19424  odfval  19564  dprdfeq0  20056  isnirred  20436  isirred2  20437  isnzr2  20534  isdomn5  20726  isdomn2OLD  20728  isdomn3  20731  drngmul0orOLD  20777  drngmuleq0  20779  sdrgacs  20818  lvecvs0or  21127  lvecvscan  21130  domnchr  21564  gsummoncoe1  22327  dmatmul  22518  mulmarep1gsum2  22595  mdetunilem8  22640  mp2pm2mplem4  22830  fvmptnn04if  22870  elcls  23096  opnnei  23143  ist0-3  23368  ist1-2  23370  dfconn2  23442  cnconn  23445  pthaus  23661  xkohaus  23676  hausflim  24004  cldsubg  24134  bcth  25376  ioorinv  25624  tdeglem4  26113  fta1b  26225  plydivex  26353  aalioulem3  26390  dvradcnv  26478  cxpcl  26730  recxpcl  26731  logrec  26820  isosctrlem2  26876  efrlim  27026  efrlimOLD  27027  muval2  27191  musum  27248  dchrelbas2  27295  dchrelbas4  27301  dchrfi  27313  dchrptlem3  27324  dchrsum2  27326  sumdchr2  27328  lgscllem  27362  2sqb  27490  2sqcoprm  27493  dchrvmasumiflem2  27560  rpvmasum2  27570  padicabv  27688  padicabvf  27689  padicabvcxp  27690  sltval2  27715  sltres  27721  noseponlem  27723  nosepon  27724  nosepeq  27744  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetasuplem4  27795  noetainflem4  27799  eln0s  28372  dfnns2  28376  tglowdim1i  28523  tgbtwnconn1  28597  colline  28671  colmid  28710  lmimid  28816  lmiisolem  28818  brbtwn2  28934  colinearalg  28939  axlowdimlem6  28976  axlowdimlem14  28984  axcontlem12  29004  incistruhgr  29110  umgr2edg1  29242  nb3grprlem1  29411  1egrvtxdg0  29543  vtxdginducedm1lem4  29574  wlkdlem4  29717  lfgriswlk  29720  pthdlem2  29800  wwlksnext  29922  clwwlknclwwlkdif  30007  clwlkclwwlklem2a4  30025  clwwisshclwwsn  30044  1wlkdlem4  30168  eupth2lem1  30246  eupth2lem3lem4  30259  frgr3vlem1  30301  frgr3vlem2  30302  3vfriswmgrlem  30305  4cycl2vnunb  30318  frgrncvvdeqlem8  30334  frgrregorufr  30353  frgrreg  30422  frgrregord013  30423  9p10ne21fool  30499  nvmul0or  30678  nmogtmnf  30798  hvmul0or  31053  hvmulcan  31100  hvmulcan2  31101  hiidge0  31126  bcsiALT  31207  shne0i  31476  nonbooli  31679  nmopgtmnf  31896  unopbd  32043  nmcfnlbi  32080  nmopcoi  32123  chirredi  32422  mdsymlem5  32435  sumdmdlem2  32447  n0nsnel  32542  disji2f  32596  aciunf1  32679  hashxpe  32816  elrgspnlem2  33232  ply1dg3rt0irred  33586  sitgaddlemb  34329  sgn3da  34522  plymulx  34541  bnj1109  34778  bnj1542  34849  bnj1253  35009  dff15  35076  lfuhgr3  35103  dfacycgr1  35128  subfacp1lem6  35169  cvmsdisj  35254  satffunlem1lem1  35386  satffunlem2lem1  35388  satffun  35393  btwnconn1lem13  36080  lineunray  36128  rankeq1o  36152  elicc3  36299  nn0prpw  36305  ordtoplem  36417  bj-snmoore  37095  irrdifflemf  37307  icorempo  37333  matunitlindflem1  37602  poimirlem1  37607  poimirlem14  37620  poimirlem16  37622  poimirlem19  37625  poimirlem23  37629  poimirlem25  37631  poimirlem26  37632  itg2addnclem3  37659  itgaddnclem2  37665  fdc  37731  ismgmOLD  37836  cvrval2  39255  cvrnbtwn2  39256  cvrnbtwn3  39257  cvlsupr3  39325  cvrat4  39425  2at0mat0  39507  dalawlem13  39865  isltrn2N  40102  trlator0  40153  cdleme22b  40323  dochkrshp  41368  dochkrshp4  41371  lcfl6  41482  lclkrlem2x  41512  hashnexinj  42109  rspcsbnea  42112  aks6d1c5  42120  metakunt6  42191  metakunt7  42192  metakunt11  42196  metakunt22  42207  nnn1suc  42279  expeqidd  42338  remullid  42439  fimgmcyc  42520  infdesc  42629  fphpd  42803  jm2.23  42984  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  44409  onfrALTlem5  44539  onfrALTlem3  44541  en3lpVD  44842  onfrALTlem5VD  44882  onfrALTlem3VD  44884  ax6e2ndeqVD  44906  ax6e2ndeqALT  44928  isosctrlem1ALT  44931  ndisj2  44990  limsupre2lem  45679  cncfiooicclem1  45848  iblcncfioo  45933  stoweidlem28  45983  sge0iunmpt  46373  n0nsn2el  46974  afvfv0bi  47101  2ffzoeq  47276  iccpartiltu  47346  iccpartlt  47348  icceuelpartlem  47359  lighneallem4  47534  oddprmALTV  47611  evenprm2  47638  odd2prm2  47642  even3prm2  47643  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  upgrwlkupwlk  47983  copisnmnd  48012  pgrpgt2nabl  48210  islindeps  48298  lincext1  48299  lindslinindsimp2lem5  48307  snlindsntor  48316  ldepslinc  48354  m1modmmod  48370  rrx2linest  48591  line2ylem  48600  line2xlem  48602