Definition df-ne 2960

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

This definition is referenced by:  neii  2961  neir  2962  nne  2963  neneqd  2964  neqned  2966  eqneqall  2970  necon2bd  2975  necon1bd  2977  necon3d  2980  necon2d  2982  necon1bi  2987  necon1i  2992  necon3abid  2995  necon1bbid  2998  necon3bid  3003  necon3abii  3005  necon3bii  3011  neor  3051  neanior  3052  neorian  3054  nfne  3060  nfned  3061  nabbib  3062  nelb  3240  dfpss2  4043  dfdif3OLD  4074  n0f  4303  n0  4307  abn0  4340  2nreu  4400  raaan2  4478  ifnefalse  4494  snnzb  4679  raldifsni  4757  eqsn  4789  n0snor2el  4793  opthpr  4811  prneimg2  4815  opthprneg  4825  unissint  4932  iununi  5058  disji2  5086  opthneg  5451  otthne  5456  opab0  5527  xpcan  6164  xpcan2  6165  xpima  6170  unixpid  6273  unizlim  6472  dff14a  7256  orduniorsuc  7812  dflim3  7829  tfindsg  7843  nn0suc  7877  findsg  7880  resf1extb  7917  xpord2pred  8127  xpord2indlem  8129  frxp3  8133  suppvalbr  8146  frrlem14  8282  tz7.49  8418  oevn0  8486  fsetexb  8847  php  9177  1sdom  9201  fimaxg  9233  fiint  9273  wemapsolem  9500  card2on  9504  brwdomn0  9519  rankxplim2  9840  rankxplim3  9841  updjudhf  9891  carden2a  9926  enpr2  9962  dfackm  10125  fin1a2lem12  10370  ac6num  10438  zorn2lem4  10458  zorn2lem7  10461  brdom3  10487  iundom2g  10499  r1tskina  10742  ltlen  11286  uzm1  12875  xrnemnf  13121  xrnepnf  13122  ioo0  13376  ico0  13397  ioc0  13398  icc0  13399  fzne1  13611  elfznelfzo  13781  elfznelfzob  13782  injresinjlem  13798  fleqceilz  13866  fsuppmapnn0fiubex  14007  sq01  14240  hash1snb  14434  hashgt12el  14437  hashgt12el2  14438  hashfun  14452  hash2prde  14485  hashge2el2dif  14495  fundmge2nop0  14517  repswcshw  14827  cshw1  14837  sgn3da  15116  incexc2  15870  sqrt2irr  16283  divalglem8  16436  ndvdssub  16445  algcvgblem  16613  lcmcllem  16632  lcmfunsnlem2  16676  isprm3  16719  isprm4  16720  2mulprm  16729  ramcl2lem  17047  cshwshashlem1  17133  cshwshash  17142  smndex2dnrinv  18954  sgrp2nmndlem3  18964  sgrp2nmndlem5  18968  symg2bas  19435  odfval  19574  dprdfeq0  20066  isnirred  20471  isirred2  20472  isnzr2  20570  isdomn5  20762  isdomn2OLD  20764  isdomn3  20767  drngmul0orOLD  20813  drngmuleq0  20815  sdrgacs  20852  lvecvs0or  21180  lvecvscan  21183  domnchr  21586  gsummoncoe1  22373  dmatmul  22559  mulmarep1gsum2  22636  mdetunilem8  22681  mp2pm2mplem4  22871  fvmptnn04if  22911  elcls  23135  opnnei  23182  ist0-3  23407  ist1-2  23409  dfconn2  23481  cnconn  23484  pthaus  23700  xkohaus  23715  hausflim  24043  cldsubg  24173  bcth  25393  ioorinv  25640  tdeglem4  26122  fta1b  26234  plymulidp  26348  plydivex  26363  aalioulem3  26400  dvradcnv  26486  cxpcl  26741  recxpcl  26742  logrec  26830  isosctrlem2  26886  efrlim  27036  muval2  27200  musum  27257  dchrelbas2  27303  dchrelbas4  27309  dchrfi  27321  dchrptlem3  27332  dchrsum2  27334  sumdchr2  27336  lgscllem  27370  2sqb  27498  2sqcoprm  27501  dchrvmasumiflem2  27568  rpvmasum2  27578  padicabv  27696  padicabvf  27697  padicabvcxp  27698  ltsval2  27722  ltsres  27728  noseponlem  27730  nosepon  27731  nosepeq  27751  nosupbnd2lem1  27781  noinfbnd2lem1  27796  noetasuplem4  27802  noetainflem4  27806  eln0s  28456  dfnns2  28467  bdayfinbndlem1  28562  tglowdim1i  28672  tgbtwnconn1  28746  colline  28821  colmid  28863  lmimid  28969  lmiisolem  28971  brbtwn2  29108  colinearalg  29113  axlowdimlem6  29150  axlowdimlem14  29158  axcontlem12  29178  incistruhgr  29282  umgr2edg1  29414  nb3grprlem1  29583  1egrvtxdg0  29714  vtxdginducedm1lem4  29745  wlkdlem4  29886  lfgriswlk  29889  pthdlem2  29970  wwlksnext  30095  clwwlknclwwlkdif  30183  clwlkclwwlklem2a4  30201  clwwisshclwwsn  30220  1wlkdlem4  30344  eupth2lem1  30422  eupth2lem3lem4  30435  frgr3vlem1  30477  frgr3vlem2  30478  3vfriswmgrlem  30481  4cycl2vnunb  30494  frgrncvvdeqlem8  30510  frgrregorufr  30529  frgrreg  30598  frgrregord013  30599  9p10ne21fool  30675  nvmul0or  30855  nmogtmnf  30975  hvmul0or  31230  hvmulcan  31277  hvmulcan2  31278  hiidge0  31303  bcsiALT  31384  shne0i  31653  nonbooli  31856  nmopgtmnf  32073  unopbd  32220  nmcfnlbi  32257  nmopcoi  32300  chirredi  32599  mdsymlem5  32612  sumdmdlem2  32624  n0nsnel  32716  disji2f  32779  aciunf1  32867  hashxpe  33011  elrgspnlem2  33426  ply1dg3rt0irred  33782  extdgfialglem1  33991  sitgaddlemb  34647  bnj1109  35084  bnj1542  35154  bnj1253  35314  dff15  35380  lfuhgr3  35475  dfacycgr1  35499  subfacp1lem6  35540  cvmsdisj  35625  satffunlem1lem1  35757  satffunlem2lem1  35759  satffun  35764  btwnconn1lem13  36454  lineunray  36502  rankeq1o  36526  elicc3  36682  nn0prpw  36688  ordtoplem  36800  bj-snmoore  37608  irrdifflemf  37822  qdiffALT  37825  icorempo  37850  matunitlindflem1  38120  poimirlem1  38125  poimirlem14  38138  poimirlem16  38140  poimirlem19  38143  poimirlem23  38147  poimirlem25  38149  poimirlem26  38150  itg2addnclem3  38177  itgaddnclem2  38183  fdc  38249  ismgmOLD  38354  cvrval2  39903  cvrnbtwn2  39904  cvrnbtwn3  39905  cvlsupr3  39973  cvrat4  40072  2at0mat0  40154  dalawlem13  40512  isltrn2N  40749  trlator0  40800  cdleme22b  40970  dochkrshp  42015  dochkrshp4  42018  lcfl6  42129  lclkrlem2x  42159  hashnexinj  42750  rspcsbnea  42753  aks6d1c5  42761  nnn1suc  42886  expeqidd  42939  remullid  43048  fimgmcyc  43157  infdesc  43230  fphpd  43398  jm2.23  43578  dflim6  43846  onsucf1olem  43852  onov0suclim  43856  oenassex  43900  tfsconcatb0  43926  tfsconcat0b  43928  naddwordnexlem4  43983  safesnsupfilb  43999  faosnf0.11b  44008  dfsucon  44104  iunrelexp0  44283  ntrneineine1lem  44665  pm13.196a  44995  onfrALTlem5  45123  onfrALTlem3  45125  en3lpVD  45425  onfrALTlem5VD  45465  onfrALTlem3VD  45467  ax6e2ndeqVD  45489  ax6e2ndeqALT  45511  isosctrlem1ALT  45514  rext0  45519  dfac5prim  45571  modelac8prim  45573  permac8prim  45595  ndisj2  45636  limsupre2lem  46303  cncfiooicclem1  46472  iblcncfioo  46557  stoweidlem28  46607  sge0iunmpt  46997  chnerlem1  47463  n0nsn2el  47624  afvfv0bi  47751  2ffzoeq  47927  m1modmmod  47963  modm1p1ne  47975  iccpartiltu  48033  iccpartlt  48035  icceuelpartlem  48046  lighneallem4  48224  oddprmALTV  48314  evenprm2  48341  odd2prm2  48345  even3prm2  48346  upgrimpthslem2  48535  gpg5nbgrvtx03starlem1  48695  gpg5nbgrvtx03starlem2  48696  gpg5nbgrvtx03starlem3  48697  gpg5nbgrvtx13starlem1  48698  gpg5nbgrvtx13starlem2  48699  gpg5nbgrvtx13starlem3  48700  pg4cyclnex  48754  gpg5edgnedg  48757  upgrwlkupwlk  48767  copisnmnd  48796  pgrpgt2nabl  48993  islindeps  49080  lincext1  49081  lindslinindsimp2lem5  49089  snlindsntor  49098  ldepslinc  49136  rrx2linest  49369  line2ylem  49378  line2xlem  49380  oppcmndclem  49643