Definition df-ne 2956

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

This definition is used by:  neii  2957  neir  2958  nne  2959  neneqd  2960  neqned  2962  eqneqall  2966  necon2bd  2971  necon1bd  2973  necon3d  2976  necon2d  2978  necon1bi  2983  necon1i  2988  necon3abid  2991  necon1bbid  2994  necon3bid  2999  necon3abii  3001  necon3bii  3007  neor  3047  neanior  3048  neorian  3050  nfne  3058  nfned  3059  nabbib  3060  nelb  3238  dfpss2  4035  n0f  4295  n0  4299  abn0  4333  2nreu  4401  raaan2  4477  ifnefalse  4493  snnzb  4678  raldifsni  4757  eqsn  4789  n0snor2el  4792  opthpr  4810  prneimg2  4814  opthprneg  4824  unissint  4931  iununi  5058  disji2  5086  opthneg  5449  otthne  5454  opab0  5525  xpcan  6163  xpcan2  6164  xpima  6169  unixpid  6276  unizlim  6476  fvtp0  7194  dff14a  7262  dff15  7264  orduniorsuc  7824  dflim3  7841  tfindsg  7855  nn0suc  7889  findsg  7892  resf1extb  7929  xpord2pred  8140  xpord2indlem  8142  frxp3  8146  suppvalbr  8159  frrlem14  8295  tz7.49  8433  oevn0  8501  fsetexb  8864  php  9200  1sdom  9224  fimaxg  9256  fiint  9296  wemapsolem  9522  card2on  9526  brwdomn0  9541  rankxplim2  9870  rankxplim3  9871  updjudhf  9983  carden2a  10018  enpr2  10054  dfackm  10216  fin1a2lem12  10460  ac6num  10528  zorn2lem4  10548  zorn2lem7  10551  brdom3  10578  iundom2g  10595  r1tskina  10838  ltlen  11382  uzm1  12968  xrnemnf  13215  xrnepnf  13216  ioo0  13470  ico0  13491  ioc0  13492  icc0  13493  fzne1  13706  elfznelfzo  13876  elfznelfzob  13877  injresinjlem  13893  fleqceilz  13962  fsuppmapnn0fiubex  14103  sq01  14336  hash1snb  14531  hashgt12el  14534  hashgt12el2  14535  hashfun  14549  hash2prde  14582  hashge2el2dif  14592  fundmge2nop0  14614  repswcshw  14930  cshw1  14940  sgn3da  15221  incexc2  15974  sqrt2irr  16384  divalglem8  16537  ndvdssub  16546  algcvgblem  16714  lcmcllem  16733  lcmfunsnlem2  16777  isprm3  16820  isprm4  16821  2mulprm  16830  ramcl2lem  17148  cshwshashlem1  17234  cshwshash  17243  smndex2dnrinv  19075  sgrp2nmndlem3  19085  sgrp2nmndlem5  19089  symg2bas  19568  odfval  19707  dprdfeq0  20199  isnirred  20611  isirred2  20612  isnzr2  20729  isdomn5  20923  isdomn3  20927  drngmuleq0  20981  sdrgacs  21019  lvecvs0or  21347  lvecvscan  21350  domnchr  21799  gsummoncoe1  22587  dmatmul  22773  mulmarep1gsum2  22850  mdetunilem8  22895  matunitlindflem1  22955  mp2pm2mplem4  23088  fvmptnn04if  23128  elcls  23352  opnnei  23399  ist0-3  23624  ist1-2  23626  dfconn2  23698  cnconn  23701  pthaus  23918  xkohaus  23933  hausflim  24261  cldsubg  24391  bcth  25611  ioorinv  25858  tdeglem4  26339  fta1b  26451  plymulidp  26566  plydivex  26581  rnplynfin  26593  plyconz  26594  aalioulem3  26624  dvradcnv  26711  cxpcl  26965  recxpcl  26966  logrec  27054  isosctrlem2  27110  efrlim  27260  muval2  27424  musum  27481  dchrelbas2  27527  dchrelbas4  27533  dchrfi  27545  dchrptlem3  27556  dchrsum2  27558  sumdchr2  27560  lgscllem  27594  2sqb  27722  2sqcoprm  27725  dchrvmasumiflem2  27792  rpvmasum2  27802  padicabv  27920  padicabvf  27921  padicabvcxp  27922  ltsval2  27946  ltsres  27952  noseponlem  27954  nosepon  27955  nosepeq  27975  nosupbnd2lem1  28005  noinfbnd2lem1  28020  noetasuplem4  28026  noetainflem4  28030  eln0s  28680  dfnns2  28691  bdayfinbndlem1  28786  tglowdim1i  28897  tgbtwnconn1  28971  colline  29051  colmid  29093  lmimid  29232  lmiisolem  29234  brbtwn2  29416  colinearalg  29421  axlowdimlem6  29458  axlowdimlem14  29466  axcontlem12  29486  incistruhgr  29590  lfuhgr3  29661  umgr2edg1  29725  nb3grprlem1  29894  1egrvtxdg0  30025  vtxdginducedm1lem4  30056  wlkdlem4  30197  lfgriswlk  30204  pthdlem2  30287  wwlksnext  30415  clwwlknclwwlkdif  30503  clwlkclwwlklem2a4  30521  clwwisshclwwsn  30540  1wlkdlem4  30664  dfacycgr1  30683  eupth2lem1  30752  eupth2lem3lem4  30765  frgr3vlem1  30807  frgr3vlem2  30808  3vfriswmgrlem  30811  4cycl2vnunb  30824  frgrncvvdeqlem8  30840  frgrregorufr  30859  frgrreg  30928  frgrregord013  30929  9p10ne21fool  31005  nvmul0or  31185  nmogtmnf  31305  hvmul0or  31560  hvmulcan  31607  hvmulcan2  31608  hiidge0  31633  bcsiALT  31714  shne0i  31983  nonbooli  32186  nmopgtmnf  32403  unopbd  32550  nmcfnlbi  32587  nmopcoi  32630  chirredi  32929  mdsymlem5  32942  sumdmdlem2  32954  n0nsnel  33044  disji2f  33104  aciunf1  33190  hashxpe  33332  elrgspnlem2  33737  ply1dg3rt0irred  34049  extdgfialglem1  34257  sitgaddlemb  34914  bnj1109  35351  bnj1542  35421  bnj1253  35581  subfacp1lem6  35871  cvmsdisj  35956  satffunlem1lem1  36088  satffunlem2lem1  36090  satffun  36095  btwnconn1lem13  36786  lineunray  36834  rankeq1o  36854  nmulel1  36886  elicc3  37027  nn0prpw  37033  ordtoplem  37145  bj-snmoore  37954  irrdifflemf  38166  qdiffALT  38169  icorempo  38194  poimirlem1  38459  poimirlem14  38472  poimirlem16  38474  poimirlem19  38477  poimirlem23  38481  poimirlem25  38483  poimirlem26  38484  itg2addnclem3  38511  itgaddnclem2  38517  fdc  38599  ismgmOLD  38704  cvrval2  40251  cvrnbtwn2  40252  cvrnbtwn3  40253  cvlsupr3  40321  cvrat4  40420  2at0mat0  40502  dalawlem13  40860  isltrn2N  41097  trlator0  41148  cdleme22b  41318  dochkrshp  42363  dochkrshp4  42366  lcfl6  42477  lclkrlem2x  42507  hashnexinj  43098  rspcsbnea  43101  aks6d1c5  43109  nnn1suc  43251  expeqidd  43304  remullid  43413  fimgmcyc  43520  infdesc  43593  fphpd  43761  jm2.23  43941  dflim6  44209  onsucf1olem  44215  onov0suclim  44219  oenassex  44263  tfsconcatb0  44289  tfsconcat0b  44291  naddwordnexlem4  44346  safesnsupfilb  44362  faosnf0.11b  44371  dfsucon  44467  iunrelexp0  44646  ntrneineine1lem  45028  pm13.196a  45342  onfrALTlem5  45469  onfrALTlem3  45471  en3lpVD  45771  onfrALTlem5VD  45811  onfrALTlem3VD  45813  ax6e2ndeqVD  45835  ax6e2ndeqALT  45857  isosctrlem1ALT  45860  rext0  45865  dfac5prim  45917  modelac8prim  45919  permac8prim  45941  ndisj2  45989  limsupre2lem  46656  cncfiooicclem1  46825  iblcncfioo  46910  stoweidlem28  46960  sge0iunmpt  47350  chnerlem1  47814  n0nsn2el  48017  afvfv0bi  48144  2ffzoeq  48320  m1modmmod  48356  modm1p1ne  48368  iccpartiltu  48426  iccpartlt  48428  icceuelpartlem  48439  lighneallem4  48617  oddprmALTV  48707  evenprm2  48734  odd2prm2  48738  even3prm2  48739  upgrimpthslem2  48928  gpg5nbgrvtx03starlem1  49088  gpg5nbgrvtx03starlem2  49089  gpg5nbgrvtx03starlem3  49090  gpg5nbgrvtx13starlem1  49091  gpg5nbgrvtx13starlem2  49092  gpg5nbgrvtx13starlem3  49093  pg4cyclnex  49147  gpg5edgnedg  49150  upgrwlkupwlk  49160  copisnmnd  49188  pgrpgt2nabl  49400  islindeps  49487  lincext1  49488  lindslinindsimp2lem5  49496  snlindsntor  49505  ldepslinc  49543  rrx2linest  49776  line2ylem  49785  line2xlem  49787  oppcmndclem  50047