Definition df-ne 2941

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 2940	. 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  2942  neir  2943  nne  2944  neneqd  2945  neqned  2947  eqneqall  2951  necon2bd  2956  necon1bd  2958  necon3d  2961  necon2d  2963  necon1bi  2969  necon1i  2974  necon3abid  2977  necon1bbid  2980  necon3bid  2985  necon3abii  2987  necon3bii  2993  neor  3034  neanior  3035  neorian  3037  nfne  3043  nfned  3044  nabbib  3045  nelb  3234  nelbOLD  3235  dfpss2  4088  dfdif3OLD  4118  n0f  4349  n0  4353  abn0  4385  2nreu  4444  raaan2  4521  ifnefalse  4537  snnzb  4718  raldifsni  4795  eqsn  4829  n0snor2el  4833  opthpr  4851  prneimg2  4855  opthprneg  4865  unissint  4972  iununi  5099  disji2  5127  opthneg  5486  otthne  5491  opab0  5559  xpcan  6196  xpcan2  6197  xpima  6202  unixpid  6304  unizlim  6507  dff14a  7290  orduniorsuc  7850  dflim3  7868  tfindsg  7882  nn0suc  7916  findsg  7919  resf1extb  7956  xpord2pred  8170  xpord2indlem  8172  frxp3  8176  suppvalbr  8189  frrlem14  8324  wfrlem16OLD  8364  tz7.49  8485  oevn0  8553  fsetexb  8904  php  9247  phpOLD  9259  1sdom  9284  1sdomOLD  9285  fimaxg  9323  fiint  9366  fiintOLD  9367  wemapsolem  9590  card2on  9594  brwdomn0  9609  rankxplim2  9920  rankxplim3  9921  updjudhf  9971  carden2a  10006  enpr2  10042  dfackm  10207  fin1a2lem12  10451  ac6num  10519  zorn2lem4  10539  zorn2lem7  10542  brdom3  10568  iundom2g  10580  r1tskina  10822  1re  11261  ltlen  11362  uzm1  12916  xrnemnf  13159  xrnepnf  13160  ioo0  13412  ico0  13433  ioc0  13434  icc0  13435  fzne1  13644  elfznelfzo  13811  elfznelfzob  13812  injresinjlem  13826  fleqceilz  13894  fsuppmapnn0fiubex  14033  sq01  14264  hash1snb  14458  hashgt12el  14461  hashgt12el2  14462  hashfun  14476  hash2prde  14509  hashge2el2dif  14519  fundmge2nop0  14541  repswcshw  14850  cshw1  14860  incexc2  15874  sqrt2irr  16285  divalglem8  16437  ndvdssub  16446  algcvgblem  16614  lcmcllem  16633  lcmfunsnlem2  16677  isprm3  16720  isprm4  16721  2mulprm  16730  ramcl2lem  17047  cshwshashlem1  17133  cshwshash  17142  smndex2dnrinv  18928  sgrp2nmndlem3  18938  sgrp2nmndlem5  18942  symg2bas  19410  odfval  19550  dprdfeq0  20042  isnirred  20420  isirred2  20421  isnzr2  20518  isdomn5  20710  isdomn2OLD  20712  isdomn3  20715  drngmul0orOLD  20761  drngmuleq0  20763  sdrgacs  20802  lvecvs0or  21110  lvecvscan  21113  domnchr  21547  gsummoncoe1  22312  dmatmul  22503  mulmarep1gsum2  22580  mdetunilem8  22625  mp2pm2mplem4  22815  fvmptnn04if  22855  elcls  23081  opnnei  23128  ist0-3  23353  ist1-2  23355  dfconn2  23427  cnconn  23430  pthaus  23646  xkohaus  23661  hausflim  23989  cldsubg  24119  bcth  25363  ioorinv  25611  tdeglem4  26099  fta1b  26211  plydivex  26339  aalioulem3  26376  dvradcnv  26464  cxpcl  26716  recxpcl  26717  logrec  26806  isosctrlem2  26862  efrlim  27012  efrlimOLD  27013  muval2  27177  musum  27234  dchrelbas2  27281  dchrelbas4  27287  dchrfi  27299  dchrptlem3  27310  dchrsum2  27312  sumdchr2  27314  lgscllem  27348  2sqb  27476  2sqcoprm  27479  dchrvmasumiflem2  27546  rpvmasum2  27556  padicabv  27674  padicabvf  27675  padicabvcxp  27676  sltval2  27701  sltres  27707  noseponlem  27709  nosepon  27710  nosepeq  27730  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  eln0s  28358  dfnns2  28362  tglowdim1i  28509  tgbtwnconn1  28583  colline  28657  colmid  28696  lmimid  28802  lmiisolem  28804  brbtwn2  28920  colinearalg  28925  axlowdimlem6  28962  axlowdimlem14  28970  axcontlem12  28990  incistruhgr  29096  umgr2edg1  29228  nb3grprlem1  29397  1egrvtxdg0  29529  vtxdginducedm1lem4  29560  wlkdlem4  29703  lfgriswlk  29706  pthdlem2  29788  wwlksnext  29913  clwwlknclwwlkdif  29998  clwlkclwwlklem2a4  30016  clwwisshclwwsn  30035  1wlkdlem4  30159  eupth2lem1  30237  eupth2lem3lem4  30250  frgr3vlem1  30292  frgr3vlem2  30293  3vfriswmgrlem  30296  4cycl2vnunb  30309  frgrncvvdeqlem8  30325  frgrregorufr  30344  frgrreg  30413  frgrregord013  30414  9p10ne21fool  30490  nvmul0or  30669  nmogtmnf  30789  hvmul0or  31044  hvmulcan  31091  hvmulcan2  31092  hiidge0  31117  bcsiALT  31198  shne0i  31467  nonbooli  31670  nmopgtmnf  31887  unopbd  32034  nmcfnlbi  32071  nmopcoi  32114  chirredi  32413  mdsymlem5  32426  sumdmdlem2  32438  n0nsnel  32534  disji2f  32590  aciunf1  32673  hashxpe  32811  elrgspnlem2  33247  ply1dg3rt0irred  33607  sitgaddlemb  34350  sgn3da  34544  plymulx  34563  bnj1109  34800  bnj1542  34871  bnj1253  35031  dff15  35098  lfuhgr3  35125  dfacycgr1  35149  subfacp1lem6  35190  cvmsdisj  35275  satffunlem1lem1  35407  satffunlem2lem1  35409  satffun  35414  btwnconn1lem13  36100  lineunray  36148  rankeq1o  36172  elicc3  36318  nn0prpw  36324  ordtoplem  36436  bj-snmoore  37114  irrdifflemf  37326  icorempo  37352  matunitlindflem1  37623  poimirlem1  37628  poimirlem14  37641  poimirlem16  37643  poimirlem19  37646  poimirlem23  37650  poimirlem25  37652  poimirlem26  37653  itg2addnclem3  37680  itgaddnclem2  37686  fdc  37752  ismgmOLD  37857  cvrval2  39275  cvrnbtwn2  39276  cvrnbtwn3  39277  cvlsupr3  39345  cvrat4  39445  2at0mat0  39527  dalawlem13  39885  isltrn2N  40122  trlator0  40173  cdleme22b  40343  dochkrshp  41388  dochkrshp4  41391  lcfl6  41502  lclkrlem2x  41532  hashnexinj  42129  rspcsbnea  42132  aks6d1c5  42140  metakunt6  42211  metakunt7  42212  metakunt11  42216  metakunt22  42227  nnn1suc  42301  expeqidd  42360  remullid  42463  fimgmcyc  42544  infdesc  42653  fphpd  42827  jm2.23  43008  dflim6  43277  onsucf1olem  43283  onov0suclim  43287  oenassex  43331  tfsconcatb0  43357  tfsconcat0b  43359  naddwordnexlem4  43414  safesnsupfilb  43431  faosnf0.11b  43440  dfsucon  43536  iunrelexp0  43715  ntrneineine1lem  44097  pm13.196a  44433  onfrALTlem5  44562  onfrALTlem3  44564  en3lpVD  44865  onfrALTlem5VD  44905  onfrALTlem3VD  44907  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  isosctrlem1ALT  44954  rext0  44959  dfac5prim  45007  modelac8prim  45009  ndisj2  45056  limsupre2lem  45739  cncfiooicclem1  45908  iblcncfioo  45993  stoweidlem28  46043  sge0iunmpt  46433  n0nsn2el  47037  afvfv0bi  47164  2ffzoeq  47339  iccpartiltu  47409  iccpartlt  47411  icceuelpartlem  47422  lighneallem4  47597  oddprmALTV  47674  evenprm2  47701  odd2prm2  47705  even3prm2  47706  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  upgrwlkupwlk  48056  copisnmnd  48085  pgrpgt2nabl  48282  islindeps  48370  lincext1  48371  lindslinindsimp2lem5  48379  snlindsntor  48388  ldepslinc  48426  m1modmmod  48442  rrx2linest  48663  line2ylem  48672  line2xlem  48674  oppcmndclem  48905