Definition df-ne 3017

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

This definition is referenced by:  neii  3018  neir  3019  nne  3020  neneqd  3021  neqned  3023  eqneqall  3027  necon2bd  3032  necon1bd  3034  necon3d  3037  necon2d  3039  necon1bi  3044  necon1i  3049  necon3abid  3052  necon1bbid  3055  necon3bid  3060  necon3abii  3062  necon3bii  3068  neor  3108  neanior  3109  neorian  3111  nfne  3119  nfned  3120  nabbi  3121  nelb  3268  dfpss2  4062  dfdif3  4091  n0f  4307  2nreu  4393  raaan2  4464  ifnefalse  4479  snnzb  4654  raldifsni  4728  eqsn  4762  n0snor2el  4764  opthpr  4782  opthprneg  4795  unissint  4900  iununi  5021  disji2  5048  opthneg  5373  opab0  5441  xpcan  6033  xpcan2  6034  xpima  6039  unixpid  6135  unizlim  6307  dff14a  7028  orduniorsuc  7545  dflim3  7562  tfindsg  7575  nn0suc  7606  findsg  7609  suppvalbr  7834  wfrlem16  7970  tz7.49  8081  oevn0  8140  php  8701  1sdom  8721  fimaxg  8765  fiint  8795  wemapsolem  9014  card2on  9018  brwdomn0  9033  rankxplim2  9309  rankxplim3  9310  updjudhf  9360  carden2a  9395  dfackm  9592  fin1a2lem12  9833  ac6num  9901  zorn2lem4  9921  zorn2lem7  9924  brdom3  9950  iundom2g  9962  r1tskina  10204  1re  10641  ltlen  10741  uzm1  12277  xrnemnf  12513  xrnepnf  12514  ioo0  12764  ico0  12785  ioc0  12786  icc0  12787  elfznelfzo  13143  elfznelfzob  13144  injresinjlem  13158  fleqceilz  13223  fsuppmapnn0fiubex  13361  sq01  13587  hash1snb  13781  hashgt12el  13784  hashgt12el2  13785  hashfun  13799  hash2prde  13829  hashge2el2dif  13839  fundmge2nop0  13851  repswcshw  14174  cshw1  14184  incexc2  15193  sqrt2irr  15602  divalglem8  15751  ndvdssub  15760  algcvgblem  15921  lcmcllem  15940  lcmfunsnlem2  15984  isprm3  16027  isprm4  16028  2mulprm  16037  ramcl2lem  16345  cshwshashlem1  16429  cshwshash  16438  smndex2dnrinv  18080  sgrp2nmndlem3  18090  sgrp2nmndlem5  18094  symg2bas  18521  odfval  18660  dprdfeq0  19144  isnirred  19450  isirred2  19451  drngmul0or  19523  drngmuleq0  19525  sdrgacs  19580  lvecvs0or  19880  lvecvscan  19883  isnzr2  20036  isdomn2  20072  gsummoncoe1  20472  domnchr  20679  dmatmul  21106  mulmarep1gsum2  21183  mdetunilem8  21228  mp2pm2mplem4  21417  fvmptnn04if  21457  elcls  21681  opnnei  21728  ist0-3  21953  ist1-2  21955  dfconn2  22027  cnconn  22030  pthaus  22246  xkohaus  22261  hausflim  22589  cldsubg  22719  bcth  23932  ioorinv  24177  tdeglem4  24654  fta1b  24763  plydivex  24886  aalioulem3  24923  dvradcnv  25009  cxpcl  25257  recxpcl  25258  logrec  25341  isosctrlem2  25397  efrlim  25547  muval2  25711  musum  25768  dchrelbas2  25813  dchrelbas4  25819  dchrfi  25831  dchrptlem3  25842  dchrsum2  25844  sumdchr2  25846  lgscllem  25880  2sqb  26008  2sqcoprm  26011  dchrvmasumiflem2  26078  rpvmasum2  26088  padicabv  26206  padicabvf  26207  padicabvcxp  26208  tglowdim1i  26287  tgbtwnconn1  26361  colline  26435  colmid  26474  lmimid  26580  lmiisolem  26582  brbtwn2  26691  colinearalg  26696  axlowdimlem6  26733  axlowdimlem14  26741  axcontlem12  26761  incistruhgr  26864  umgr2edg1  26993  nb3grprlem1  27162  1egrvtxdg0  27293  vtxdginducedm1lem4  27324  wlkdlem4  27467  lfgriswlk  27470  pthdlem2  27549  wwlksnext  27671  clwwlknclwwlkdif  27757  clwlkclwwlklem2a4  27775  clwwisshclwwsn  27794  1wlkdlem4  27919  eupth2lem1  27997  eupth2lem3lem4  28010  frgr3vlem1  28052  frgr3vlem2  28053  3vfriswmgrlem  28056  4cycl2vnunb  28069  frgrncvvdeqlem8  28085  frgrregorufr  28104  frgrreg  28173  frgrregord013  28174  9p10ne21fool  28250  nvmul0or  28427  nmogtmnf  28547  hvmul0or  28802  hvmulcan  28849  hvmulcan2  28850  hiidge0  28875  bcsiALT  28956  shne0i  29225  nonbooli  29428  nmopgtmnf  29645  unopbd  29792  nmcfnlbi  29829  nmopcoi  29872  chirredi  30171  mdsymlem5  30184  sumdmdlem2  30196  nelbOLD  30232  disji2f  30327  aciunf1  30408  fzne1  30511  hashxpe  30529  sitgaddlemb  31606  sgn3da  31799  plymulx  31818  bnj1109  32058  bnj1542  32129  bnj1253  32289  dff15  32353  lfuhgr3  32366  dfacycgr1  32391  subfacp1lem6  32432  cvmsdisj  32517  satffunlem1lem1  32649  satffunlem2lem1  32651  satffun  32656  frrlem14  33136  sltval2  33163  sltres  33169  noseponlem  33171  nosepon  33172  nosepeq  33189  nosupbnd2lem1  33215  noetalem3  33219  btwnconn1lem13  33560  lineunray  33608  rankeq1o  33632  elicc3  33665  nn0prpw  33671  ordtoplem  33783  bj-snmoore  34408  icorempo  34635  matunitlindflem1  34903  poimirlem1  34908  poimirlem14  34921  poimirlem16  34923  poimirlem19  34926  poimirlem23  34930  poimirlem25  34932  poimirlem26  34933  itg2addnclem3  34960  itgaddnclem2  34966  fdc  35035  ismgmOLD  35143  cvrval2  36425  cvrnbtwn2  36426  cvrnbtwn3  36427  cvlsupr3  36495  cvrat4  36594  2at0mat0  36676  dalawlem13  37034  isltrn2N  37271  trlator0  37322  cdleme22b  37492  dochkrshp  38537  dochkrshp4  38540  lcfl6  38651  lclkrlem2x  38681  nnn1suc  39208  sn-00id  39280  remulid2  39298  fphpd  39462  jm2.23  39642  isdomn3  39853  dfsucon  39938  iunrelexp0  40096  ntrneineine1lem  40483  pm13.196a  40795  onfrALTlem5  40925  onfrALTlem3  40927  en3lpVD  41228  onfrALTlem5VD  41268  onfrALTlem3VD  41270  ax6e2ndeqVD  41292  ax6e2ndeqALT  41314  isosctrlem1ALT  41317  ndisj2  41362  limsupre2lem  42054  cncfiooicclem1  42225  iblcncfioo  42312  stoweidlem28  42362  sge0iunmpt  42749  afvfv0bi  43400  2ffzoeq  43577  iccpartiltu  43631  iccpartlt  43633  icceuelpartlem  43644  lighneallem4  43824  oddprmALTV  43901  evenprm2  43928  odd2prm2  43932  even3prm2  43933  upgrwlkupwlk  44064  copisnmnd  44125  pgrpgt2nabl  44463  islindeps  44557  lincext1  44558  lindslinindsimp2lem5  44566  snlindsntor  44575  ldepslinc  44613  m1modmmod  44630  rrx2linest  44778  line2ylem  44787  line2xlem  44789