Definition df-ne 2979

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

This definition is referenced by:  neii  2980  neir  2981  nne  2982  neneqd  2983  neqned  2985  eqneqall  2989  necon2bd  2994  necon1bd  2996  necon3d  2999  necon2d  3001  necon1bi  3006  necon1i  3011  necon3abid  3014  necon1bbid  3017  necon3bid  3022  necon3abii  3024  necon3bii  3030  neor  3069  neanior  3070  neorian  3072  nfne  3078  nfned  3079  nabbi  3080  dfpss2  3890  dfdif3  3919  n0f  4129  ifnefalse  4291  snnzb  4445  raldifsni  4516  eqsn  4550  n0snor2el  4552  opthpr  4571  opthprneg  4587  unissint  4693  iununi  4802  disji2  4828  opthneg  5139  opab0  5202  xpcan  5781  xpcan2  5782  xpima  5787  unixpid  5884  unizlim  6053  2f1fvneq  6737  dff14a  6747  orduniorsuc  7256  dflim3  7273  tfindsg  7286  nn0suc  7316  findsg  7319  suppvalbr  7529  wfrlem16  7662  tz7.49  7772  oevn0  7828  php  8379  1sdom  8398  fimaxg  8442  fiint  8472  wemapsolem  8690  card2on  8694  brwdomn0  8709  domwdom  8714  rankxplim2  8986  rankxplim3  8987  updjudhf  9036  carden2a  9071  dfackm  9269  fin23lem14  9436  fin1a2lem12  9514  axcc2lem  9539  ac6num  9582  zorn2lem4  9602  zorn2lem7  9605  brdom3  9631  iundom2g  9643  r1tskina  9885  1re  10321  ltlen  10419  uzm1  11932  xrnemnf  12163  xrnepnf  12164  ioo0  12414  ico0  12435  ioc0  12436  icc0  12437  elfznelfzo  12793  elfznelfzob  12794  injresinjlem  12808  fleqceilz  12873  fsuppmapnn0fiubex  13011  sq01  13205  hash1snb  13420  hashgt12el  13423  hashgt12el2  13424  hashfun  13437  hash2prde  13465  hashge2el2dif  13475  fundmge2nop0  13487  ccat1st1st  13622  swrdccatin1  13703  repswcshw  13778  cshw1  13788  xptrrel  13940  incexc2  14788  sqrt2irr  15195  divalglem8  15339  ndvdssub  15348  algcvgblem  15505  lcmcllem  15524  lcmfunsnlem2lem2  15567  lcmfunsnlem2  15568  ncoprmgcdne1b  15578  isprm3  15610  isprm4  15611  ramcl2lem  15926  cshwshashlem1  16010  cshwshash  16019  sgrp2nmndlem3  17613  sgrp2rid2  17614  sgrp2nmndlem5  17617  symg2bas  18015  symgextf  18034  symgextfv  18035  odlem1  18151  gexlem1  18191  dprdfeq0  18619  isnirred  18898  isirred2  18899  drngmul0or  18968  drngmuleq0  18970  lvecvs0or  19311  lvecvscan  19314  isnzr2  19468  isdomn2  19504  cply1mul  19868  gsummoncoe1  19878  domnchr  20084  psgndiflemB  20150  dmatmul  20510  mulmarep1gsum1  20586  mulmarep1gsum2  20587  mdetdiag  20612  mdetunilem8  20632  mdetunilem9  20633  madurid  20657  mp2pm2mplem4  20823  fvmptnn04if  20863  fvmptnn04ifb  20865  elcls  21087  opnnei  21134  ist0-3  21359  ist1-2  21361  dfconn2  21432  cnconn  21435  pthaus  21651  xkohaus  21666  hausflim  21994  cldsubg  22123  bcth  23334  ioorinv  23553  tdeglem4  24030  fta1b  24139  plydivex  24262  plyexmo  24278  aalioulem3  24299  dvradcnv  24385  logtayllem  24615  logtayl  24616  cxpcl  24630  recxpcl  24631  logrec  24711  isosctrlem2  24759  efrlim  24906  muval2  25070  musum  25127  dchrelbas2  25172  dchrelbas4  25178  dchrfi  25190  dchrptlem3  25201  dchrsum2  25203  sumdchr2  25205  lgscllem  25239  2sqb  25367  dchrvmasumiflem2  25401  rpvmasum2  25411  padicabv  25529  padicabvf  25530  padicabvcxp  25531  tglowdim1i  25606  tgbtwnconn1  25680  colline  25754  colmid  25793  lmimid  25896  lmiisolem  25898  brbtwn2  25995  colinearalg  26000  axlowdimlem6  26037  axlowdimlem14  26045  axcontlem12  26065  incistruhgr  26184  umgr2edg1  26314  nb3grprlem1  26494  1egrvtxdg0  26631  vtxdginducedm1lem4  26662  wlkdlem4  26806  lfgriswlk  26809  pthdlem2  26888  wwlksnext  27026  clwwlknclwwlkdif  27116  clwlkclwwlklem2a4  27136  clwwisshclwwsn  27155  1wlkdlem4  27309  eupth2lem1  27387  eupth2lem3lem4  27400  frgr3vlem1  27444  frgr3vlem2  27445  3vfriswmgrlem  27448  4cycl2vnunb  27461  frgrncvvdeqlem8  27477  frgrregorufr  27496  frgrreg  27578  frgrregord013  27579  nvmul0or  27829  nmogtmnf  27949  hvmul0or  28206  hvmulcan  28253  hvmulcan2  28254  hiidge0  28279  bcsiALT  28360  shne0i  28631  nonbooli  28834  nmopgtmnf  29051  unopbd  29198  nmcfnlbi  29235  nmopcoi  29278  chirredi  29577  mdsymlem5  29590  sumdmdlem2  29602  disji2f  29711  imadifxp  29735  aciunf1  29786  2sqcoprm  29968  sitgaddlemb  30731  sgn3da  30924  plymulx  30946  bnj1109  31175  bnj1542  31245  bnj1253  31403  subfacp1lem6  31485  cvmsdisj  31570  sltval2  32125  sltres  32131  noseponlem  32133  nosepon  32134  nosepeq  32151  nosupbnd2lem1  32177  noetalem3  32181  btwnconn1lem13  32522  lineunray  32570  rankeq1o  32594  elicc3  32627  nn0prpw  32634  ordtoplem  32746  bj-ismooredr2  33371  bj-snmoore  33374  icorempt2  33510  matunitlindflem1  33713  poimirlem1  33718  poimirlem14  33731  poimirlem16  33733  poimirlem19  33736  poimirlem23  33740  poimirlem25  33742  poimirlem26  33743  itg2addnclem3  33770  itgaddnclem2  33776  fdc  33847  ismgmOLD  33955  cvrval2  35049  cvrnbtwn2  35050  cvrnbtwn3  35051  cvlsupr3  35119  cvrat4  35218  2at0mat0  35300  dalawlem13  35658  isltrn2N  35895  trlator0  35946  cdleme22b  36116  dochkrshp  37161  dochkrshp4  37164  lcfl6  37275  lclkrlem2x  37305  fphpd  37876  jm2.23  38058  sdrgacs  38266  isdomn3  38277  iunrelexp0  38488  ntrneineine1lem  38876  pm13.196a  39108  onfrALTlem5  39249  onfrALTlem3  39251  en3lpVD  39568  onfrALTlem5VD  39609  onfrALTlem3VD  39611  ax6e2ndeqVD  39633  ax6e2ndeqALT  39655  isosctrlem1ALT  39658  ndisj2  39705  limsupre2lem  40430  cncfiooicclem1  40580  iblcncfioo  40667  stoweidlem28  40718  sge0iunmpt  41108  raaan2  41643  afvfv0bi  41735  2ffzoeq  41907  iccpartiltu  41927  iccpartlt  41929  icceuelpartlem  41940  cshword2  42006  lighneallem4  42096  oddprmALTV  42167  evenprm2  42192  odd2prm2  42196  even3prm2  42197  upgrwlkupwlk  42283  copisnmnd  42371  pgrpgt2nabl  42709  islindeps  42804  lincext1  42805  lindslinindsimp2lem5  42813  snlindsntor  42822  ldepslinc  42860  m1modmmod  42878