Definition df-ne 2931

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

This definition is referenced by:  neii  2932  neir  2933  nne  2934  neneqd  2935  neqned  2937  eqneqall  2941  necon2bd  2946  necon1bd  2948  necon3d  2951  necon2d  2953  necon1bi  2959  necon1i  2964  necon3abid  2967  necon1bbid  2970  necon3bid  2975  necon3abii  2977  necon3bii  2983  neor  3024  neanior  3025  neorian  3027  nfne  3033  nfned  3034  nabbib  3035  nelb  3222  nelbOLD  3223  dfpss2  4081  dfdif3  4110  n0f  4342  n0  4346  abn0  4378  2nreu  4438  raaan2  4519  ifnefalse  4535  snnzb  4717  raldifsni  4794  eqsn  4828  n0snor2el  4832  opthpr  4850  opthprneg  4863  unissint  4972  iununi  5099  disji2  5127  opthneg  5477  otthne  5482  opab0  5550  xpcan  6177  xpcan2  6178  xpima  6183  unixpid  6285  unizlim  6488  dff14a  7274  orduniorsuc  7828  dflim3  7846  tfindsg  7860  nn0suc  7896  findsg  7899  xpord2pred  8148  xpord2indlem  8150  frxp3  8154  suppvalbr  8167  frrlem14  8303  wfrlem16OLD  8343  tz7.49  8464  oevn0  8534  fsetexb  8882  php  9234  phpOLD  9246  1sdom  9272  1sdomOLD  9273  fimaxg  9314  fiint  9358  fiintOLD  9359  wemapsolem  9583  card2on  9587  brwdomn0  9602  rankxplim2  9913  rankxplim3  9914  updjudhf  9964  carden2a  9999  enpr2  10035  dfackm  10199  fin1a2lem12  10442  ac6num  10510  zorn2lem4  10530  zorn2lem7  10533  brdom3  10559  iundom2g  10571  r1tskina  10813  1re  11252  ltlen  11353  uzm1  12903  xrnemnf  13142  xrnepnf  13143  ioo0  13394  ico0  13415  ioc0  13416  icc0  13417  elfznelfzo  13783  elfznelfzob  13784  injresinjlem  13798  fleqceilz  13865  fsuppmapnn0fiubex  14003  sq01  14234  hash1snb  14428  hashgt12el  14431  hashgt12el2  14432  hashfun  14446  hash2prde  14481  hashge2el2dif  14491  fundmge2nop0  14503  repswcshw  14812  cshw1  14822  incexc2  15834  sqrt2irr  16243  divalglem8  16394  ndvdssub  16403  algcvgblem  16570  lcmcllem  16589  lcmfunsnlem2  16633  isprm3  16676  isprm4  16677  2mulprm  16686  ramcl2lem  17003  cshwshashlem1  17090  cshwshash  17099  smndex2dnrinv  18897  sgrp2nmndlem3  18907  sgrp2nmndlem5  18911  symg2bas  19383  odfval  19523  dprdfeq0  20015  isnirred  20395  isirred2  20396  isnzr2  20493  isdomn5  20681  isdomn2OLD  20683  isdomn3  20686  drngmul0orOLD  20732  drngmuleq0  20734  sdrgacs  20773  lvecvs0or  21082  lvecvscan  21085  domnchr  21519  gsummoncoe1  22293  dmatmul  22484  mulmarep1gsum2  22561  mdetunilem8  22606  mp2pm2mplem4  22796  fvmptnn04if  22836  elcls  23062  opnnei  23109  ist0-3  23334  ist1-2  23336  dfconn2  23408  cnconn  23411  pthaus  23627  xkohaus  23642  hausflim  23970  cldsubg  24100  bcth  25342  ioorinv  25590  tdeglem4  26080  tdeglem4OLD  26081  fta1b  26193  plydivex  26319  aalioulem3  26356  dvradcnv  26444  cxpcl  26695  recxpcl  26696  logrec  26785  isosctrlem2  26841  efrlim  26991  efrlimOLD  26992  muval2  27156  musum  27213  dchrelbas2  27260  dchrelbas4  27266  dchrfi  27278  dchrptlem3  27289  dchrsum2  27291  sumdchr2  27293  lgscllem  27327  2sqb  27455  2sqcoprm  27458  dchrvmasumiflem2  27525  rpvmasum2  27535  padicabv  27653  padicabvf  27654  padicabvcxp  27655  sltval2  27680  sltres  27686  noseponlem  27688  nosepon  27689  nosepeq  27709  nosupbnd2lem1  27739  noinfbnd2lem1  27754  noetasuplem4  27760  noetainflem4  27764  eln0s  28318  tglowdim1i  28422  tgbtwnconn1  28496  colline  28570  colmid  28609  lmimid  28715  lmiisolem  28717  brbtwn2  28833  colinearalg  28838  axlowdimlem6  28875  axlowdimlem14  28883  axcontlem12  28903  incistruhgr  29009  umgr2edg1  29141  nb3grprlem1  29310  1egrvtxdg0  29442  vtxdginducedm1lem4  29473  wlkdlem4  29616  lfgriswlk  29619  pthdlem2  29699  wwlksnext  29821  clwwlknclwwlkdif  29906  clwlkclwwlklem2a4  29924  clwwisshclwwsn  29943  1wlkdlem4  30067  eupth2lem1  30145  eupth2lem3lem4  30158  frgr3vlem1  30200  frgr3vlem2  30201  3vfriswmgrlem  30204  4cycl2vnunb  30217  frgrncvvdeqlem8  30233  frgrregorufr  30252  frgrreg  30321  frgrregord013  30322  9p10ne21fool  30398  nvmul0or  30577  nmogtmnf  30697  hvmul0or  30952  hvmulcan  30999  hvmulcan2  31000  hiidge0  31025  bcsiALT  31106  shne0i  31375  nonbooli  31578  nmopgtmnf  31795  unopbd  31942  nmcfnlbi  31979  nmopcoi  32022  chirredi  32321  mdsymlem5  32334  sumdmdlem2  32346  n0nsnel  32439  disji2f  32494  aciunf1  32577  fzne1  32690  hashxpe  32711  ply1dg3rt0irred  33457  sitgaddlemb  34192  sgn3da  34385  plymulx  34404  bnj1109  34641  bnj1542  34712  bnj1253  34872  dff15  34931  lfuhgr3  34957  dfacycgr1  34982  subfacp1lem6  35023  cvmsdisj  35108  satffunlem1lem1  35240  satffunlem2lem1  35242  satffun  35247  btwnconn1lem13  35933  lineunray  35981  rankeq1o  36005  elicc3  36039  nn0prpw  36045  ordtoplem  36157  bj-snmoore  36830  irrdifflemf  37042  icorempo  37068  matunitlindflem1  37327  poimirlem1  37332  poimirlem14  37345  poimirlem16  37347  poimirlem19  37350  poimirlem23  37354  poimirlem25  37356  poimirlem26  37357  itg2addnclem3  37384  itgaddnclem2  37390  fdc  37456  ismgmOLD  37561  cvrval2  38982  cvrnbtwn2  38983  cvrnbtwn3  38984  cvlsupr3  39052  cvrat4  39152  2at0mat0  39234  dalawlem13  39592  isltrn2N  39829  trlator0  39880  cdleme22b  40050  dochkrshp  41095  dochkrshp4  41098  lcfl6  41209  lclkrlem2x  41239  hashnexinj  41837  rspcsbnea  41840  aks6d1c5  41848  metakunt6  41915  metakunt7  41916  metakunt11  41920  metakunt22  41931  nnn1suc  42002  expeqidd  42048  remullid  42141  fimgmcyc  42221  infdesc  42330  fphpd  42507  jm2.23  42688  dflim6  42964  onsucf1olem  42970  onov0suclim  42974  oenassex  43018  tfsconcatb0  43044  tfsconcat0b  43046  naddwordnexlem4  43102  safesnsupfilb  43119  faosnf0.11b  43128  dfsucon  43224  iunrelexp0  43403  ntrneineine1lem  43785  pm13.196a  44122  onfrALTlem5  44252  onfrALTlem3  44254  en3lpVD  44555  onfrALTlem5VD  44595  onfrALTlem3VD  44597  ax6e2ndeqVD  44619  ax6e2ndeqALT  44641  isosctrlem1ALT  44644  ndisj2  44686  limsupre2lem  45378  cncfiooicclem1  45547  iblcncfioo  45632  stoweidlem28  45682  sge0iunmpt  46072  n0nsn2el  46673  afvfv0bi  46798  2ffzoeq  46973  iccpartiltu  47027  iccpartlt  47029  icceuelpartlem  47040  lighneallem4  47215  oddprmALTV  47292  evenprm2  47319  odd2prm2  47323  even3prm2  47324  upgrwlkupwlk  47550  copisnmnd  47579  pgrpgt2nabl  47778  islindeps  47869  lincext1  47870  lindslinindsimp2lem5  47878  snlindsntor  47887  ldepslinc  47925  m1modmmod  47942  rrx2linest  48163  line2ylem  48172  line2xlem  48174