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  3213  dfpss2  4041  dfdif3OLD  4071  n0f  4302  n0  4306  abn0  4338  2nreu  4397  raaan2  4476  ifnefalse  4492  snnzb  4676  raldifsni  4752  eqsn  4786  n0snor2el  4790  opthpr  4808  prneimg2  4812  opthprneg  4822  unissint  4928  iununi  5055  disji2  5083  opthneg  5430  otthne  5435  opab0  5503  xpcan  6135  xpcan2  6136  xpima  6141  unixpid  6243  unizlim  6442  dff14a  7218  orduniorsuc  7774  dflim3  7791  tfindsg  7805  nn0suc  7838  findsg  7841  resf1extb  7878  xpord2pred  8089  xpord2indlem  8091  frxp3  8095  suppvalbr  8108  frrlem14  8243  tz7.49  8378  oevn0  8444  fsetexb  8805  php  9135  1sdom  9159  fimaxg  9191  fiint  9231  wemapsolem  9459  card2on  9463  brwdomn0  9478  rankxplim2  9796  rankxplim3  9797  updjudhf  9847  carden2a  9882  enpr2  9918  dfackm  10081  fin1a2lem12  10325  ac6num  10393  zorn2lem4  10413  zorn2lem7  10416  brdom3  10442  iundom2g  10454  r1tskina  10697  ltlen  11238  uzm1  12789  xrnemnf  13035  xrnepnf  13036  ioo0  13290  ico0  13311  ioc0  13312  icc0  13313  fzne1  13524  elfznelfzo  13693  elfznelfzob  13694  injresinjlem  13710  fleqceilz  13778  fsuppmapnn0fiubex  13919  sq01  14152  hash1snb  14346  hashgt12el  14349  hashgt12el2  14350  hashfun  14364  hash2prde  14397  hashge2el2dif  14407  fundmge2nop0  14429  repswcshw  14739  cshw1  14749  incexc2  15765  sqrt2irr  16178  divalglem8  16331  ndvdssub  16340  algcvgblem  16508  lcmcllem  16527  lcmfunsnlem2  16571  isprm3  16614  isprm4  16615  2mulprm  16624  ramcl2lem  16941  cshwshashlem1  17027  cshwshash  17036  smndex2dnrinv  18844  sgrp2nmndlem3  18854  sgrp2nmndlem5  18858  symg2bas  19326  odfval  19465  dprdfeq0  19957  isnirred  20360  isirred2  20361  isnzr2  20455  isdomn5  20647  isdomn2OLD  20649  isdomn3  20652  drngmul0orOLD  20698  drngmuleq0  20700  sdrgacs  20738  lvecvs0or  21067  lvecvscan  21070  domnchr  21491  gsummoncoe1  22256  dmatmul  22445  mulmarep1gsum2  22522  mdetunilem8  22567  mp2pm2mplem4  22757  fvmptnn04if  22797  elcls  23021  opnnei  23068  ist0-3  23293  ist1-2  23295  dfconn2  23367  cnconn  23370  pthaus  23586  xkohaus  23601  hausflim  23929  cldsubg  24059  bcth  25289  ioorinv  25537  tdeglem4  26025  fta1b  26137  plydivex  26265  aalioulem3  26302  dvradcnv  26390  cxpcl  26643  recxpcl  26644  logrec  26733  isosctrlem2  26789  efrlim  26939  efrlimOLD  26940  muval2  27104  musum  27161  dchrelbas2  27208  dchrelbas4  27214  dchrfi  27226  dchrptlem3  27237  dchrsum2  27239  sumdchr2  27241  lgscllem  27275  2sqb  27403  2sqcoprm  27406  dchrvmasumiflem2  27473  rpvmasum2  27483  padicabv  27601  padicabvf  27602  padicabvcxp  27603  ltsval2  27628  ltsres  27634  noseponlem  27636  nosepon  27637  nosepeq  27657  nosupbnd2lem1  27687  noinfbnd2lem1  27702  noetasuplem4  27708  noetainflem4  27712  eln0s  28361  dfnns2  28372  bdayfinbndlem1  28467  tglowdim1i  28577  tgbtwnconn1  28651  colline  28725  colmid  28764  lmimid  28870  lmiisolem  28872  brbtwn2  28982  colinearalg  28987  axlowdimlem6  29024  axlowdimlem14  29032  axcontlem12  29052  incistruhgr  29156  umgr2edg1  29288  nb3grprlem1  29457  1egrvtxdg0  29589  vtxdginducedm1lem4  29620  wlkdlem4  29761  lfgriswlk  29764  pthdlem2  29845  wwlksnext  29970  clwwlknclwwlkdif  30058  clwlkclwwlklem2a4  30076  clwwisshclwwsn  30095  1wlkdlem4  30219  eupth2lem1  30297  eupth2lem3lem4  30310  frgr3vlem1  30352  frgr3vlem2  30353  3vfriswmgrlem  30356  4cycl2vnunb  30369  frgrncvvdeqlem8  30385  frgrregorufr  30404  frgrreg  30473  frgrregord013  30474  9p10ne21fool  30550  nvmul0or  30729  nmogtmnf  30849  hvmul0or  31104  hvmulcan  31151  hvmulcan2  31152  hiidge0  31177  bcsiALT  31258  shne0i  31527  nonbooli  31730  nmopgtmnf  31947  unopbd  32094  nmcfnlbi  32131  nmopcoi  32174  chirredi  32473  mdsymlem5  32486  sumdmdlem2  32498  n0nsnel  32593  disji2f  32655  aciunf1  32744  hashxpe  32889  sgn3da  32917  elrgspnlem2  33327  ply1dg3rt0irred  33667  extdgfialglem1  33851  sitgaddlemb  34507  plymulx  34707  bnj1109  34944  bnj1542  35015  bnj1253  35175  dff15  35242  lfuhgr3  35316  dfacycgr1  35340  subfacp1lem6  35381  cvmsdisj  35466  satffunlem1lem1  35598  satffunlem2lem1  35600  satffun  35605  btwnconn1lem13  36295  lineunray  36343  rankeq1o  36367  elicc3  36513  nn0prpw  36519  ordtoplem  36631  bj-snmoore  37320  irrdifflemf  37532  icorempo  37558  matunitlindflem1  37819  poimirlem1  37824  poimirlem14  37837  poimirlem16  37839  poimirlem19  37842  poimirlem23  37846  poimirlem25  37848  poimirlem26  37849  itg2addnclem3  37876  itgaddnclem2  37882  fdc  37948  ismgmOLD  38053  cvrval2  39602  cvrnbtwn2  39603  cvrnbtwn3  39604  cvlsupr3  39672  cvrat4  39771  2at0mat0  39853  dalawlem13  40211  isltrn2N  40448  trlator0  40499  cdleme22b  40669  dochkrshp  41714  dochkrshp4  41717  lcfl6  41828  lclkrlem2x  41858  hashnexinj  42450  rspcsbnea  42453  aks6d1c5  42461  nnn1suc  42588  expeqidd  42647  remullid  42756  fimgmcyc  42856  infdesc  42953  fphpd  43125  jm2.23  43305  dflim6  43573  onsucf1olem  43579  onov0suclim  43583  oenassex  43627  tfsconcatb0  43653  tfsconcat0b  43655  naddwordnexlem4  43710  safesnsupfilb  43726  faosnf0.11b  43735  dfsucon  43831  iunrelexp0  44010  ntrneineine1lem  44392  pm13.196a  44722  onfrALTlem5  44850  onfrALTlem3  44852  en3lpVD  45152  onfrALTlem5VD  45192  onfrALTlem3VD  45194  ax6e2ndeqVD  45216  ax6e2ndeqALT  45238  isosctrlem1ALT  45241  rext0  45246  dfac5prim  45298  modelac8prim  45300  permac8prim  45322  ndisj2  45363  limsupre2lem  46035  cncfiooicclem1  46204  iblcncfioo  46289  stoweidlem28  46339  sge0iunmpt  46729  chnerlem1  47193  n0nsn2el  47338  afvfv0bi  47465  2ffzoeq  47640  m1modmmod  47671  modm1p1ne  47683  iccpartiltu  47735  iccpartlt  47737  icceuelpartlem  47748  lighneallem4  47923  oddprmALTV  48000  evenprm2  48027  odd2prm2  48031  even3prm2  48032  upgrimpthslem2  48221  gpg5nbgrvtx03starlem1  48381  gpg5nbgrvtx03starlem2  48382  gpg5nbgrvtx03starlem3  48383  gpg5nbgrvtx13starlem1  48384  gpg5nbgrvtx13starlem2  48385  gpg5nbgrvtx13starlem3  48386  pg4cyclnex  48440  gpg5edgnedg  48443  upgrwlkupwlk  48453  copisnmnd  48482  pgrpgt2nabl  48679  islindeps  48766  lincext1  48767  lindslinindsimp2lem5  48775  snlindsntor  48784  ldepslinc  48822  rrx2linest  49055  line2ylem  49064  line2xlem  49066  oppcmndclem  49329