Definition df-ne 2944

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

This definition is referenced by:  neii  2945  neir  2946  nne  2947  neneqd  2948  neqned  2950  eqneqall  2954  necon2bd  2959  necon1bd  2961  necon3d  2964  necon2d  2966  necon1bi  2972  necon1i  2977  necon3abid  2980  necon1bbid  2983  necon3bid  2988  necon3abii  2990  necon3bii  2996  neor  3036  neanior  3037  neorian  3039  nfne  3045  nfned  3046  nabbi  3047  nelb  3195  nelbOLD  3196  dfpss2  4017  dfdif3  4046  n0f  4274  n0  4278  abn0  4312  2nreu  4373  raaan2  4453  ifnefalse  4468  snnzb  4651  raldifsni  4725  eqsn  4759  n0snor2el  4761  opthpr  4779  opthprneg  4792  unissint  4900  iununi  5024  disji2  5052  opthneg  5389  opab0  5459  xpcan  6067  xpcan2  6068  xpima  6073  unixpid  6175  unizlim  6365  dff14a  7121  orduniorsuc  7649  dflim3  7666  tfindsg  7679  nn0suc  7713  findsg  7717  suppvalbr  7949  frrlem14  8082  wfrlem16  8112  tz7.49  8223  oevn0  8284  fsetexb  8587  php  8874  1sdom  8929  fimaxg  8966  fiint  8996  wemapsolem  9214  card2on  9218  brwdomn0  9233  rankxplim2  9544  rankxplim3  9545  updjudhf  9595  carden2a  9630  dfackm  9828  fin1a2lem12  10073  ac6num  10141  zorn2lem4  10161  zorn2lem7  10164  brdom3  10190  iundom2g  10202  r1tskina  10444  1re  10881  ltlen  10981  uzm1  12520  xrnemnf  12757  xrnepnf  12758  ioo0  13008  ico0  13029  ioc0  13030  icc0  13031  elfznelfzo  13395  elfznelfzob  13396  injresinjlem  13410  fleqceilz  13477  fsuppmapnn0fiubex  13615  sq01  13843  hash1snb  14037  hashgt12el  14040  hashgt12el2  14041  hashfun  14055  hash2prde  14087  hashge2el2dif  14097  fundmge2nop0  14109  repswcshw  14428  cshw1  14438  incexc2  15453  sqrt2irr  15861  divalglem8  16012  ndvdssub  16021  algcvgblem  16185  lcmcllem  16204  lcmfunsnlem2  16248  isprm3  16291  isprm4  16292  2mulprm  16301  ramcl2lem  16613  cshwshashlem1  16700  cshwshash  16709  smndex2dnrinv  18444  sgrp2nmndlem3  18454  sgrp2nmndlem5  18458  symg2bas  18890  odfval  19030  dprdfeq0  19515  isnirred  19832  isirred2  19833  drngmul0or  19902  drngmuleq0  19904  sdrgacs  19959  lvecvs0or  20260  lvecvscan  20263  isnzr2  20422  isdomn2  20458  domnchr  20623  gsummoncoe1  21360  dmatmul  21529  mulmarep1gsum2  21606  mdetunilem8  21651  mp2pm2mplem4  21841  fvmptnn04if  21881  elcls  22107  opnnei  22154  ist0-3  22379  ist1-2  22381  dfconn2  22453  cnconn  22456  pthaus  22672  xkohaus  22687  hausflim  23015  cldsubg  23145  bcth  24373  ioorinv  24620  tdeglem4  25104  tdeglem4OLD  25105  fta1b  25214  plydivex  25337  aalioulem3  25374  dvradcnv  25460  cxpcl  25709  recxpcl  25710  logrec  25793  isosctrlem2  25849  efrlim  25999  muval2  26163  musum  26220  dchrelbas2  26265  dchrelbas4  26271  dchrfi  26283  dchrptlem3  26294  dchrsum2  26296  sumdchr2  26298  lgscllem  26332  2sqb  26460  2sqcoprm  26463  dchrvmasumiflem2  26530  rpvmasum2  26540  padicabv  26658  padicabvf  26659  padicabvcxp  26660  tglowdim1i  26741  tgbtwnconn1  26815  colline  26889  colmid  26928  lmimid  27034  lmiisolem  27036  brbtwn2  27151  colinearalg  27156  axlowdimlem6  27193  axlowdimlem14  27201  axcontlem12  27221  incistruhgr  27327  umgr2edg1  27456  nb3grprlem1  27625  1egrvtxdg0  27756  vtxdginducedm1lem4  27787  wlkdlem4  27930  lfgriswlk  27933  pthdlem2  28012  wwlksnext  28134  clwwlknclwwlkdif  28219  clwlkclwwlklem2a4  28237  clwwisshclwwsn  28256  1wlkdlem4  28380  eupth2lem1  28458  eupth2lem3lem4  28471  frgr3vlem1  28513  frgr3vlem2  28514  3vfriswmgrlem  28517  4cycl2vnunb  28530  frgrncvvdeqlem8  28546  frgrregorufr  28565  frgrreg  28634  frgrregord013  28635  9p10ne21fool  28711  nvmul0or  28888  nmogtmnf  29008  hvmul0or  29263  hvmulcan  29310  hvmulcan2  29311  hiidge0  29336  bcsiALT  29417  shne0i  29686  nonbooli  29889  nmopgtmnf  30106  unopbd  30253  nmcfnlbi  30290  nmopcoi  30333  chirredi  30632  mdsymlem5  30645  sumdmdlem2  30657  nelbOLDOLD  30693  disji2f  30792  aciunf1  30877  fzne1  30986  hashxpe  31004  sitgaddlemb  32190  sgn3da  32383  plymulx  32402  bnj1109  32641  bnj1542  32712  bnj1253  32872  dff15  32931  lfuhgr3  32956  dfacycgr1  32981  subfacp1lem6  33022  cvmsdisj  33107  satffunlem1lem1  33239  satffunlem2lem1  33241  satffun  33246  xpord2pred  33694  xpord2ind  33696  poxp3  33698  frxp3  33699  xpord3pred  33700  sltval2  33761  sltres  33767  noseponlem  33769  nosepon  33770  nosepeq  33790  nosupbnd2lem1  33820  noinfbnd2lem1  33835  noetasuplem4  33841  noetainflem4  33845  btwnconn1lem13  34303  lineunray  34351  rankeq1o  34375  elicc3  34408  nn0prpw  34414  ordtoplem  34526  bj-snmoore  35187  irrdifflemf  35399  icorempo  35428  matunitlindflem1  35679  poimirlem1  35684  poimirlem14  35697  poimirlem16  35699  poimirlem19  35702  poimirlem23  35706  poimirlem25  35708  poimirlem26  35709  itg2addnclem3  35736  itgaddnclem2  35742  fdc  35809  ismgmOLD  35914  cvrval2  37194  cvrnbtwn2  37195  cvrnbtwn3  37196  cvlsupr3  37264  cvrat4  37363  2at0mat0  37445  dalawlem13  37803  isltrn2N  38040  trlator0  38091  cdleme22b  38261  dochkrshp  39306  dochkrshp4  39309  lcfl6  39420  lclkrlem2x  39450  metakunt6  40030  metakunt7  40031  metakunt11  40035  metakunt22  40046  isdomn5  40071  nnn1suc  40189  sn-00id  40277  remulid2  40308  infdesc  40368  fphpd  40526  jm2.23  40706  isdomn3  40917  dfsucon  41000  iunrelexp0  41172  ntrneineine1lem  41556  pm13.196a  41894  onfrALTlem5  42024  onfrALTlem3  42026  en3lpVD  42327  onfrALTlem5VD  42367  onfrALTlem3VD  42369  ax6e2ndeqVD  42391  ax6e2ndeqALT  42413  isosctrlem1ALT  42416  ndisj2  42461  limsupre2lem  43128  cncfiooicclem1  43297  iblcncfioo  43382  stoweidlem28  43432  sge0iunmpt  43819  afvfv0bi  44504  2ffzoeq  44681  iccpartiltu  44735  iccpartlt  44737  icceuelpartlem  44748  lighneallem4  44923  oddprmALTV  45000  evenprm2  45027  odd2prm2  45031  even3prm2  45032  upgrwlkupwlk  45163  copisnmnd  45224  pgrpgt2nabl  45563  islindeps  45655  lincext1  45656  lindslinindsimp2lem5  45664  snlindsntor  45673  ldepslinc  45711  m1modmmod  45728  rrx2linest  45949  line2ylem  45958  line2xlem  45960