Definition df-ne 2988

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

This definition is referenced by:  neii  2989  neir  2990  nne  2991  neneqd  2992  neqned  2994  eqneqall  2998  necon2bd  3003  necon1bd  3005  necon3d  3008  necon2d  3010  necon1bi  3015  necon1i  3020  necon3abid  3023  necon1bbid  3026  necon3bid  3031  necon3abii  3033  necon3bii  3039  neor  3078  neanior  3079  neorian  3081  nfne  3087  nfned  3088  nabbi  3089  nelb  3227  dfpss2  4013  dfdif3  4042  n0f  4257  n0  4260  2nreu  4349  raaan2  4422  ifnefalse  4437  snnzb  4614  raldifsni  4688  eqsn  4722  n0snor2el  4724  opthpr  4742  opthprneg  4755  unissint  4862  iununi  4984  disji2  5012  opthneg  5338  opab0  5406  xpcan  6000  xpcan2  6001  xpima  6006  unixpid  6103  unizlim  6275  dff14a  7006  orduniorsuc  7525  dflim3  7542  tfindsg  7555  nn0suc  7586  findsg  7590  suppvalbr  7817  wfrlem16  7953  tz7.49  8064  oevn0  8123  php  8685  1sdom  8705  fimaxg  8749  fiint  8779  wemapsolem  8998  card2on  9002  brwdomn0  9017  rankxplim2  9293  rankxplim3  9294  updjudhf  9344  carden2a  9379  dfackm  9577  fin1a2lem12  9822  ac6num  9890  zorn2lem4  9910  zorn2lem7  9913  brdom3  9939  iundom2g  9951  r1tskina  10193  1re  10630  ltlen  10730  uzm1  12264  xrnemnf  12500  xrnepnf  12501  ioo0  12751  ico0  12772  ioc0  12773  icc0  12774  elfznelfzo  13137  elfznelfzob  13138  injresinjlem  13152  fleqceilz  13217  fsuppmapnn0fiubex  13355  sq01  13582  hash1snb  13776  hashgt12el  13779  hashgt12el2  13780  hashfun  13794  hash2prde  13824  hashge2el2dif  13834  fundmge2nop0  13846  repswcshw  14165  cshw1  14175  incexc2  15185  sqrt2irr  15594  divalglem8  15741  ndvdssub  15750  algcvgblem  15911  lcmcllem  15930  lcmfunsnlem2  15974  isprm3  16017  isprm4  16018  2mulprm  16027  ramcl2lem  16335  cshwshashlem1  16421  cshwshash  16430  smndex2dnrinv  18072  sgrp2nmndlem3  18082  sgrp2nmndlem5  18086  symg2bas  18513  odfval  18652  dprdfeq0  19137  isnirred  19446  isirred2  19447  drngmul0or  19516  drngmuleq0  19518  sdrgacs  19573  lvecvs0or  19873  lvecvscan  19876  isnzr2  20029  isdomn2  20065  domnchr  20224  gsummoncoe1  20933  dmatmul  21102  mulmarep1gsum2  21179  mdetunilem8  21224  mp2pm2mplem4  21414  fvmptnn04if  21454  elcls  21678  opnnei  21725  ist0-3  21950  ist1-2  21952  dfconn2  22024  cnconn  22027  pthaus  22243  xkohaus  22258  hausflim  22586  cldsubg  22716  bcth  23933  ioorinv  24180  tdeglem4  24661  fta1b  24770  plydivex  24893  aalioulem3  24930  dvradcnv  25016  cxpcl  25265  recxpcl  25266  logrec  25349  isosctrlem2  25405  efrlim  25555  muval2  25719  musum  25776  dchrelbas2  25821  dchrelbas4  25827  dchrfi  25839  dchrptlem3  25850  dchrsum2  25852  sumdchr2  25854  lgscllem  25888  2sqb  26016  2sqcoprm  26019  dchrvmasumiflem2  26086  rpvmasum2  26096  padicabv  26214  padicabvf  26215  padicabvcxp  26216  tglowdim1i  26295  tgbtwnconn1  26369  colline  26443  colmid  26482  lmimid  26588  lmiisolem  26590  brbtwn2  26699  colinearalg  26704  axlowdimlem6  26741  axlowdimlem14  26749  axcontlem12  26769  incistruhgr  26872  umgr2edg1  27001  nb3grprlem1  27170  1egrvtxdg0  27301  vtxdginducedm1lem4  27332  wlkdlem4  27475  lfgriswlk  27478  pthdlem2  27557  wwlksnext  27679  clwwlknclwwlkdif  27764  clwlkclwwlklem2a4  27782  clwwisshclwwsn  27801  1wlkdlem4  27925  eupth2lem1  28003  eupth2lem3lem4  28016  frgr3vlem1  28058  frgr3vlem2  28059  3vfriswmgrlem  28062  4cycl2vnunb  28075  frgrncvvdeqlem8  28091  frgrregorufr  28110  frgrreg  28179  frgrregord013  28180  9p10ne21fool  28256  nvmul0or  28433  nmogtmnf  28553  hvmul0or  28808  hvmulcan  28855  hvmulcan2  28856  hiidge0  28881  bcsiALT  28962  shne0i  29231  nonbooli  29434  nmopgtmnf  29651  unopbd  29798  nmcfnlbi  29835  nmopcoi  29878  chirredi  30177  mdsymlem5  30190  sumdmdlem2  30202  nelbOLD  30239  disji2f  30340  aciunf1  30426  fzne1  30537  hashxpe  30555  sitgaddlemb  31716  sgn3da  31909  plymulx  31928  bnj1109  32168  bnj1542  32239  bnj1253  32399  dff15  32463  lfuhgr3  32479  dfacycgr1  32504  subfacp1lem6  32545  cvmsdisj  32630  satffunlem1lem1  32762  satffunlem2lem1  32764  satffun  32769  frrlem14  33249  sltval2  33276  sltres  33282  noseponlem  33284  nosepon  33285  nosepeq  33302  nosupbnd2lem1  33328  noetalem3  33332  btwnconn1lem13  33673  lineunray  33721  rankeq1o  33745  elicc3  33778  nn0prpw  33784  ordtoplem  33896  bj-snmoore  34528  irrdifflemf  34739  icorempo  34768  matunitlindflem1  35053  poimirlem1  35058  poimirlem14  35071  poimirlem16  35073  poimirlem19  35076  poimirlem23  35080  poimirlem25  35082  poimirlem26  35083  itg2addnclem3  35110  itgaddnclem2  35116  fdc  35183  ismgmOLD  35288  cvrval2  36570  cvrnbtwn2  36571  cvrnbtwn3  36572  cvlsupr3  36640  cvrat4  36739  2at0mat0  36821  dalawlem13  37179  isltrn2N  37416  trlator0  37467  cdleme22b  37637  dochkrshp  38682  dochkrshp4  38685  lcfl6  38796  lclkrlem2x  38826  metakunt6  39355  metakunt7  39356  metakunt11  39360  metakunt22  39371  nnn1suc  39467  sn-00id  39539  remulid2  39570  fphpd  39757  jm2.23  39937  isdomn3  40148  dfsucon  40231  iunrelexp0  40403  ntrneineine1lem  40787  pm13.196a  41118  onfrALTlem5  41248  onfrALTlem3  41250  en3lpVD  41551  onfrALTlem5VD  41591  onfrALTlem3VD  41593  ax6e2ndeqVD  41615  ax6e2ndeqALT  41637  isosctrlem1ALT  41640  ndisj2  41685  limsupre2lem  42366  cncfiooicclem1  42535  iblcncfioo  42620  stoweidlem28  42670  sge0iunmpt  43057  afvfv0bi  43708  2ffzoeq  43885  iccpartiltu  43939  iccpartlt  43941  icceuelpartlem  43952  lighneallem4  44128  oddprmALTV  44205  evenprm2  44232  odd2prm2  44236  even3prm2  44237  upgrwlkupwlk  44368  copisnmnd  44429  pgrpgt2nabl  44768  islindeps  44862  lincext1  44863  lindslinindsimp2lem5  44871  snlindsntor  44880  ldepslinc  44918  m1modmmod  44935  rrx2linest  45156  line2ylem  45165  line2xlem  45167