Definition df-ne 2947

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

This definition is referenced by:  neii  2948  neir  2949  nne  2950  neneqd  2951  neqned  2953  eqneqall  2957  necon2bd  2962  necon1bd  2964  necon3d  2967  necon2d  2969  necon1bi  2975  necon1i  2980  necon3abid  2983  necon1bbid  2986  necon3bid  2991  necon3abii  2993  necon3bii  2999  neor  3040  neanior  3041  neorian  3043  nfne  3049  nfned  3050  nabbib  3051  nelb  3240  nelbOLD  3241  dfpss2  4111  dfdif3OLD  4141  n0f  4372  n0  4376  abn0  4408  2nreu  4467  raaan2  4544  ifnefalse  4560  snnzb  4743  raldifsni  4820  eqsn  4854  n0snor2el  4858  opthpr  4876  opthprneg  4889  unissint  4996  iununi  5122  disji2  5150  opthneg  5501  otthne  5506  opab0  5573  xpcan  6207  xpcan2  6208  xpima  6213  unixpid  6315  unizlim  6518  dff14a  7307  orduniorsuc  7866  dflim3  7884  tfindsg  7898  nn0suc  7934  findsg  7937  xpord2pred  8186  xpord2indlem  8188  frxp3  8192  suppvalbr  8205  frrlem14  8340  wfrlem16OLD  8380  tz7.49  8501  oevn0  8571  fsetexb  8922  php  9273  phpOLD  9285  1sdom  9311  1sdomOLD  9312  fimaxg  9351  fiint  9394  fiintOLD  9395  wemapsolem  9619  card2on  9623  brwdomn0  9638  rankxplim2  9949  rankxplim3  9950  updjudhf  10000  carden2a  10035  enpr2  10071  dfackm  10236  fin1a2lem12  10480  ac6num  10548  zorn2lem4  10568  zorn2lem7  10571  brdom3  10597  iundom2g  10609  r1tskina  10851  1re  11290  ltlen  11391  uzm1  12941  xrnemnf  13180  xrnepnf  13181  ioo0  13432  ico0  13453  ioc0  13454  icc0  13455  elfznelfzo  13822  elfznelfzob  13823  injresinjlem  13837  fleqceilz  13905  fsuppmapnn0fiubex  14043  sq01  14274  hash1snb  14468  hashgt12el  14471  hashgt12el2  14472  hashfun  14486  hash2prde  14519  hashge2el2dif  14529  fundmge2nop0  14551  repswcshw  14860  cshw1  14870  incexc2  15886  sqrt2irr  16297  divalglem8  16448  ndvdssub  16457  algcvgblem  16624  lcmcllem  16643  lcmfunsnlem2  16687  isprm3  16730  isprm4  16731  2mulprm  16740  ramcl2lem  17056  cshwshashlem1  17143  cshwshash  17152  smndex2dnrinv  18950  sgrp2nmndlem3  18960  sgrp2nmndlem5  18964  symg2bas  19434  odfval  19574  dprdfeq0  20066  isnirred  20446  isirred2  20447  isnzr2  20544  isdomn5  20732  isdomn2OLD  20734  isdomn3  20737  drngmul0orOLD  20783  drngmuleq0  20785  sdrgacs  20824  lvecvs0or  21133  lvecvscan  21136  domnchr  21570  gsummoncoe1  22333  dmatmul  22524  mulmarep1gsum2  22601  mdetunilem8  22646  mp2pm2mplem4  22836  fvmptnn04if  22876  elcls  23102  opnnei  23149  ist0-3  23374  ist1-2  23376  dfconn2  23448  cnconn  23451  pthaus  23667  xkohaus  23682  hausflim  24010  cldsubg  24140  bcth  25382  ioorinv  25630  tdeglem4  26119  fta1b  26231  plydivex  26357  aalioulem3  26394  dvradcnv  26482  cxpcl  26734  recxpcl  26735  logrec  26824  isosctrlem2  26880  efrlim  27030  efrlimOLD  27031  muval2  27195  musum  27252  dchrelbas2  27299  dchrelbas4  27305  dchrfi  27317  dchrptlem3  27328  dchrsum2  27330  sumdchr2  27332  lgscllem  27366  2sqb  27494  2sqcoprm  27497  dchrvmasumiflem2  27564  rpvmasum2  27574  padicabv  27692  padicabvf  27693  padicabvcxp  27694  sltval2  27719  sltres  27725  noseponlem  27727  nosepon  27728  nosepeq  27748  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetasuplem4  27799  noetainflem4  27803  eln0s  28376  dfnns2  28380  tglowdim1i  28527  tgbtwnconn1  28601  colline  28675  colmid  28714  lmimid  28820  lmiisolem  28822  brbtwn2  28938  colinearalg  28943  axlowdimlem6  28980  axlowdimlem14  28988  axcontlem12  29008  incistruhgr  29114  umgr2edg1  29246  nb3grprlem1  29415  1egrvtxdg0  29547  vtxdginducedm1lem4  29578  wlkdlem4  29721  lfgriswlk  29724  pthdlem2  29804  wwlksnext  29926  clwwlknclwwlkdif  30011  clwlkclwwlklem2a4  30029  clwwisshclwwsn  30048  1wlkdlem4  30172  eupth2lem1  30250  eupth2lem3lem4  30263  frgr3vlem1  30305  frgr3vlem2  30306  3vfriswmgrlem  30309  4cycl2vnunb  30322  frgrncvvdeqlem8  30338  frgrregorufr  30357  frgrreg  30426  frgrregord013  30427  9p10ne21fool  30503  nvmul0or  30682  nmogtmnf  30802  hvmul0or  31057  hvmulcan  31104  hvmulcan2  31105  hiidge0  31130  bcsiALT  31211  shne0i  31480  nonbooli  31683  nmopgtmnf  31900  unopbd  32047  nmcfnlbi  32084  nmopcoi  32127  chirredi  32426  mdsymlem5  32439  sumdmdlem2  32451  n0nsnel  32544  disji2f  32599  aciunf1  32681  fzne1  32793  hashxpe  32814  ply1dg3rt0irred  33572  sitgaddlemb  34313  sgn3da  34506  plymulx  34525  bnj1109  34762  bnj1542  34833  bnj1253  34993  dff15  35060  lfuhgr3  35087  dfacycgr1  35112  subfacp1lem6  35153  cvmsdisj  35238  satffunlem1lem1  35370  satffunlem2lem1  35372  satffun  35377  btwnconn1lem13  36063  lineunray  36111  rankeq1o  36135  elicc3  36283  nn0prpw  36289  ordtoplem  36401  bj-snmoore  37079  irrdifflemf  37291  icorempo  37317  matunitlindflem1  37576  poimirlem1  37581  poimirlem14  37594  poimirlem16  37596  poimirlem19  37599  poimirlem23  37603  poimirlem25  37605  poimirlem26  37606  itg2addnclem3  37633  itgaddnclem2  37639  fdc  37705  ismgmOLD  37810  cvrval2  39230  cvrnbtwn2  39231  cvrnbtwn3  39232  cvlsupr3  39300  cvrat4  39400  2at0mat0  39482  dalawlem13  39840  isltrn2N  40077  trlator0  40128  cdleme22b  40298  dochkrshp  41343  dochkrshp4  41346  lcfl6  41457  lclkrlem2x  41487  hashnexinj  42085  rspcsbnea  42088  aks6d1c5  42096  metakunt6  42167  metakunt7  42168  metakunt11  42172  metakunt22  42183  nnn1suc  42255  expeqidd  42312  remullid  42409  fimgmcyc  42489  infdesc  42598  fphpd  42772  jm2.23  42953  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  44383  onfrALTlem5  44513  onfrALTlem3  44515  en3lpVD  44816  onfrALTlem5VD  44856  onfrALTlem3VD  44858  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  isosctrlem1ALT  44905  ndisj2  44953  limsupre2lem  45645  cncfiooicclem1  45814  iblcncfioo  45899  stoweidlem28  45949  sge0iunmpt  46339  n0nsn2el  46940  afvfv0bi  47067  2ffzoeq  47242  iccpartiltu  47296  iccpartlt  47298  icceuelpartlem  47309  lighneallem4  47484  oddprmALTV  47561  evenprm2  47588  odd2prm2  47592  even3prm2  47593  upgrwlkupwlk  47863  copisnmnd  47892  pgrpgt2nabl  48091  islindeps  48182  lincext1  48183  lindslinindsimp2lem5  48191  snlindsntor  48200  ldepslinc  48238  m1modmmod  48255  rrx2linest  48476  line2ylem  48485  line2xlem  48487