Definition df-ne 2934

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

This definition is referenced by:  neii  2935  neir  2936  nne  2937  neneqd  2938  neqned  2940  eqneqall  2944  necon2bd  2949  necon1bd  2951  necon3d  2954  necon2d  2956  necon1bi  2961  necon1i  2966  necon3abid  2969  necon1bbid  2972  necon3bid  2977  necon3abii  2979  necon3bii  2985  neor  3025  neanior  3026  neorian  3028  nfne  3034  nfned  3035  nabbib  3036  nelb  3214  dfpss2  4029  dfdif3OLD  4059  n0f  4290  n0  4294  abn0  4326  2nreu  4385  raaan2  4463  ifnefalse  4479  snnzb  4663  raldifsni  4741  eqsn  4773  n0snor2el  4777  opthpr  4795  prneimg2  4799  opthprneg  4809  unissint  4915  iununi  5042  disji2  5070  opthneg  5433  otthne  5438  opab0  5506  xpcan  6138  xpcan2  6139  xpima  6144  unixpid  6246  unizlim  6445  dff14a  7222  orduniorsuc  7778  dflim3  7795  tfindsg  7809  nn0suc  7842  findsg  7845  resf1extb  7882  xpord2pred  8092  xpord2indlem  8094  frxp3  8098  suppvalbr  8111  frrlem14  8246  tz7.49  8381  oevn0  8447  fsetexb  8808  php  9138  1sdom  9162  fimaxg  9194  fiint  9234  wemapsolem  9462  card2on  9466  brwdomn0  9481  rankxplim2  9801  rankxplim3  9802  updjudhf  9852  carden2a  9887  enpr2  9923  dfackm  10086  fin1a2lem12  10330  ac6num  10398  zorn2lem4  10418  zorn2lem7  10421  brdom3  10447  iundom2g  10459  r1tskina  10702  ltlen  11244  uzm1  12819  xrnemnf  13065  xrnepnf  13066  ioo0  13320  ico0  13341  ioc0  13342  icc0  13343  fzne1  13555  elfznelfzo  13725  elfznelfzob  13726  injresinjlem  13742  fleqceilz  13810  fsuppmapnn0fiubex  13951  sq01  14184  hash1snb  14378  hashgt12el  14381  hashgt12el2  14382  hashfun  14396  hash2prde  14429  hashge2el2dif  14439  fundmge2nop0  14461  repswcshw  14771  cshw1  14781  incexc2  15800  sqrt2irr  16213  divalglem8  16366  ndvdssub  16375  algcvgblem  16543  lcmcllem  16562  lcmfunsnlem2  16606  isprm3  16649  isprm4  16650  2mulprm  16659  ramcl2lem  16977  cshwshashlem1  17063  cshwshash  17072  smndex2dnrinv  18883  sgrp2nmndlem3  18893  sgrp2nmndlem5  18897  symg2bas  19365  odfval  19504  dprdfeq0  19996  isnirred  20397  isirred2  20398  isnzr2  20492  isdomn5  20684  isdomn2OLD  20686  isdomn3  20689  drngmul0orOLD  20735  drngmuleq0  20737  sdrgacs  20775  lvecvs0or  21103  lvecvscan  21106  domnchr  21509  gsummoncoe1  22270  dmatmul  22459  mulmarep1gsum2  22536  mdetunilem8  22581  mp2pm2mplem4  22771  fvmptnn04if  22811  elcls  23035  opnnei  23082  ist0-3  23307  ist1-2  23309  dfconn2  23381  cnconn  23384  pthaus  23600  xkohaus  23615  hausflim  23943  cldsubg  24073  bcth  25293  ioorinv  25540  tdeglem4  26022  fta1b  26134  plydivex  26260  aalioulem3  26297  dvradcnv  26383  cxpcl  26635  recxpcl  26636  logrec  26724  isosctrlem2  26780  efrlim  26930  muval2  27094  musum  27151  dchrelbas2  27197  dchrelbas4  27203  dchrfi  27215  dchrptlem3  27226  dchrsum2  27228  sumdchr2  27230  lgscllem  27264  2sqb  27392  2sqcoprm  27395  dchrvmasumiflem2  27462  rpvmasum2  27472  padicabv  27590  padicabvf  27591  padicabvcxp  27592  ltsval2  27617  ltsres  27623  noseponlem  27625  nosepon  27626  nosepeq  27646  nosupbnd2lem1  27676  noinfbnd2lem1  27691  noetasuplem4  27697  noetainflem4  27701  eln0s  28350  dfnns2  28361  bdayfinbndlem1  28456  tglowdim1i  28566  tgbtwnconn1  28640  colline  28714  colmid  28753  lmimid  28859  lmiisolem  28861  brbtwn2  28971  colinearalg  28976  axlowdimlem6  29013  axlowdimlem14  29021  axcontlem12  29041  incistruhgr  29145  umgr2edg1  29277  nb3grprlem1  29446  1egrvtxdg0  29577  vtxdginducedm1lem4  29608  wlkdlem4  29749  lfgriswlk  29752  pthdlem2  29833  wwlksnext  29958  clwwlknclwwlkdif  30046  clwlkclwwlklem2a4  30064  clwwisshclwwsn  30083  1wlkdlem4  30207  eupth2lem1  30285  eupth2lem3lem4  30298  frgr3vlem1  30340  frgr3vlem2  30341  3vfriswmgrlem  30344  4cycl2vnunb  30357  frgrncvvdeqlem8  30373  frgrregorufr  30392  frgrreg  30461  frgrregord013  30462  9p10ne21fool  30538  nvmul0or  30718  nmogtmnf  30838  hvmul0or  31093  hvmulcan  31140  hvmulcan2  31141  hiidge0  31166  bcsiALT  31247  shne0i  31516  nonbooli  31719  nmopgtmnf  31936  unopbd  32083  nmcfnlbi  32120  nmopcoi  32163  chirredi  32462  mdsymlem5  32475  sumdmdlem2  32487  n0nsnel  32582  disji2f  32644  aciunf1  32733  hashxpe  32877  sgn3da  32904  elrgspnlem2  33301  ply1dg3rt0irred  33641  extdgfialglem1  33833  sitgaddlemb  34489  plymulx  34689  bnj1109  34926  bnj1542  34996  bnj1253  35156  dff15  35224  lfuhgr3  35299  dfacycgr1  35323  subfacp1lem6  35364  cvmsdisj  35449  satffunlem1lem1  35581  satffunlem2lem1  35583  satffun  35588  btwnconn1lem13  36278  lineunray  36326  rankeq1o  36350  elicc3  36496  nn0prpw  36502  ordtoplem  36614  bj-snmoore  37422  irrdifflemf  37636  qdiffALT  37639  icorempo  37664  matunitlindflem1  37934  poimirlem1  37939  poimirlem14  37952  poimirlem16  37954  poimirlem19  37957  poimirlem23  37961  poimirlem25  37963  poimirlem26  37964  itg2addnclem3  37991  itgaddnclem2  37997  fdc  38063  ismgmOLD  38168  cvrval2  39717  cvrnbtwn2  39718  cvrnbtwn3  39719  cvlsupr3  39787  cvrat4  39886  2at0mat0  39968  dalawlem13  40326  isltrn2N  40563  trlator0  40614  cdleme22b  40784  dochkrshp  41829  dochkrshp4  41832  lcfl6  41943  lclkrlem2x  41973  hashnexinj  42564  rspcsbnea  42567  aks6d1c5  42575  nnn1suc  42701  expeqidd  42754  remullid  42863  fimgmcyc  42976  infdesc  43073  fphpd  43241  jm2.23  43421  dflim6  43689  onsucf1olem  43695  onov0suclim  43699  oenassex  43743  tfsconcatb0  43769  tfsconcat0b  43771  naddwordnexlem4  43826  safesnsupfilb  43842  faosnf0.11b  43851  dfsucon  43947  iunrelexp0  44126  ntrneineine1lem  44508  pm13.196a  44838  onfrALTlem5  44966  onfrALTlem3  44968  en3lpVD  45268  onfrALTlem5VD  45308  onfrALTlem3VD  45310  ax6e2ndeqVD  45332  ax6e2ndeqALT  45354  isosctrlem1ALT  45357  rext0  45362  dfac5prim  45414  modelac8prim  45416  permac8prim  45438  ndisj2  45479  limsupre2lem  46149  cncfiooicclem1  46318  iblcncfioo  46403  stoweidlem28  46453  sge0iunmpt  46843  chnerlem1  47307  n0nsn2el  47464  afvfv0bi  47591  2ffzoeq  47767  m1modmmod  47803  modm1p1ne  47815  iccpartiltu  47873  iccpartlt  47875  icceuelpartlem  47886  lighneallem4  48064  oddprmALTV  48154  evenprm2  48181  odd2prm2  48185  even3prm2  48186  upgrimpthslem2  48375  gpg5nbgrvtx03starlem1  48535  gpg5nbgrvtx03starlem2  48536  gpg5nbgrvtx03starlem3  48537  gpg5nbgrvtx13starlem1  48538  gpg5nbgrvtx13starlem2  48539  gpg5nbgrvtx13starlem3  48540  pg4cyclnex  48594  gpg5edgnedg  48597  upgrwlkupwlk  48607  copisnmnd  48636  pgrpgt2nabl  48833  islindeps  48920  lincext1  48921  lindslinindsimp2lem5  48929  snlindsntor  48938  ldepslinc  48976  rrx2linest  49209  line2ylem  49218  line2xlem  49220  oppcmndclem  49483