Definition df-ne 2782

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

This definition is referenced by:  neii  2784  neir  2785  nne  2786  neneqd  2787  neqned  2789  eqneqall  2793  necon2bd  2798  necon1bd  2800  necon3d  2803  necon2d  2805  necon1bi  2810  necon1i  2815  necon3abid  2818  necon1bbid  2821  necon3bid  2826  necon3abii  2828  necon3bii  2834  neor  2873  neanior  2874  neorian  2876  nfne  2882  nfned  2883  nabbi  2884  dfpss2  3654  n0f  3886  ifnefalse  4048  snnzb  4198  raldifsni  4265  eqsn  4301  eqsnOLD  4302  n0snor2el  4304  opthpr  4324  unissint  4436  iununi  4546  disji2  4569  opthneg  4876  xpcan  5489  xpcan2  5490  xpima  5495  unixpid  5587  unizlim  5761  dff14a  6427  mpt2difsnif  6651  orduniorsuc  6922  dflim3  6939  tfindsg  6952  nn0suc  6982  findsg  6985  suppvalbr  7186  wfrlem16  7317  tz7.49  7427  oevn0  7482  php  8029  1sdom  8048  fimaxg  8092  fiint  8122  wemapsolem  8338  card2on  8342  brwdomn0  8357  domwdom  8362  rankxplim2  8626  rankxplim3  8627  carden2a  8675  dfackm  8871  fin23lem14  9038  fin1a2lem12  9116  axcc2lem  9141  ac6num  9184  zorn2lem4  9204  zorn2lem7  9207  brdom3  9231  iundom2g  9241  r1tskina  9483  1re  9918  ltlen  10017  uzm1  11594  xrnemnf  11827  xrnepnf  11828  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  elfznelfzo  12439  elfznelfzob  12440  injresinjlem  12450  fleqceilz  12515  fsuppmapnn0fiubex  12654  sq01  12848  hash1snb  13068  hashgt12el  13070  hashgt12el2  13071  hashfun  13084  hash2prde  13109  hashge2el2dif  13117  fundmge2nop0  13129  swrdccatin1  13334  repswcshw  13409  cshw1  13419  xptrrel  13567  incexc2  14409  sqrt2irr  14817  divalglem8  14961  ndvdssub  14971  algcvgblem  15128  lcmcllem  15147  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  ncoprmgcdne1b  15201  isprm2lem  15232  isprm3  15234  isprm4  15235  ramcl2lem  15551  cshwshashlem1  15640  cshwshash  15649  isnsgrp  17111  isnmnd  17121  sgrp2nmndlem3  17235  sgrp2rid2  17236  sgrp2nmndlem5  17239  symg2bas  17641  symgextf  17660  symgextfv  17661  odlem1  17777  gexlem1  17817  dprdfeq0  18244  isnirred  18523  isirred2  18524  drngmul0or  18591  drngmuleq0  18593  lvecvs0or  18929  lvecvscan  18932  isnzr2  19084  isdomn2  19120  cply1mul  19485  gsummoncoe1  19495  domnchr  19699  psgndiflemB  19765  dmatmul  20122  mulmarep1gsum1  20198  mulmarep1gsum2  20199  mdetdiag  20224  mdetunilem8  20244  mdetunilem9  20245  madurid  20269  mp2pm2mplem4  20433  fvmptnn04if  20473  fvmptnn04ifb  20475  elcls  20687  opnnei  20734  ist0-3  20959  ist1-2  20961  dfcon2  21032  cnconn  21035  pthaus  21251  xkohaus  21266  hausflim  21595  cldsubg  21724  bcth  22934  ioorinv  23150  tdeglem4  23624  fta1b  23733  plydivex  23856  plyexmo  23872  aalioulem3  23893  dvradcnv  23979  logtayllem  24205  logtayl  24206  cxpcl  24220  recxpcl  24221  logrec  24301  isosctrlem2  24349  efrlim  24496  muval2  24660  musum  24717  dchrelbas2  24762  dchrelbas4  24768  dchrfi  24780  dchrptlem3  24791  dchrsum2  24793  sumdchr2  24795  lgscllem  24829  2sqb  24957  dchrvmasumiflem2  24991  rpvmasum2  25001  padicabv  25119  padicabvf  25120  padicabvcxp  25121  tglowdim1i  25196  tgbtwnconn1  25270  colline  25344  colmid  25383  lmimid  25486  lmiisolem  25488  brbtwn2  25585  colinearalg  25590  axlowdimlem6  25627  axlowdimlem14  25635  axcontlem12  25655  incistruhgr  25746  usgra2edg1  25912  nbgranself  25963  nb3graprlem1  25980  uvtx01vtx  26020  wlkdvspthlem  26137  usgrcyclnl1  26168  usgrcyclnl2  26169  constr3trllem2  26179  wwlknext  26252  clwlkisclwwlklem2a4  26312  clwwisshclwwn  26336  clwlknclwlkdifs  26487  eupath2lem1  26504  frgra3vlem1  26527  frgra3vlem2  26528  3vfriswmgralem  26531  2pthfrgra  26538  4cycl2vnunb  26544  n4cyclfrgra  26545  frgrancvvdeqlemA  26564  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  frgraregorufr0  26579  frgraregorufr  26580  numclwwlk3lem  26635  frgrareg  26644  frgraregord013  26645  nvmul0or  26889  nmogtmnf  27009  hvmul0or  27266  hvmulcan  27313  hvmulcan2  27314  hiidge0  27339  bcsiALT  27420  shne0i  27691  nonbooli  27894  nmopgtmnf  28111  unopbd  28258  nmcfnlbi  28295  nmopcoi  28338  chirredi  28637  mdsymlem5  28650  sumdmdlem2  28662  disji2f  28772  imadifxp  28796  aciunf1  28845  2sqcoprm  28978  sitgaddlemb  29737  sgn3da  29930  plymulx  29951  bnj1109  30111  bnj1542  30181  bnj1253  30339  subfacp1lem6  30421  cvmsdisj  30506  sltval2  31053  sltres  31061  noseponlem  31065  nosepon  31066  nodenselem4  31083  nodenselem5  31084  nodenselem7  31086  nobndup  31099  nobnddown  31100  nofulllem5  31105  btwnconn1lem13  31376  lineunray  31424  rankeq1o  31448  elicc3  31481  nn0prpw  31488  ordtoplem  31604  icorempt2  32375  matunitlindflem1  32575  poimirlem1  32580  poimirlem14  32593  poimirlem16  32595  poimirlem19  32598  poimirlem23  32602  poimirlem25  32604  poimirlem26  32605  itg2addnclem3  32633  itgaddnclem2  32639  fdc  32711  ismgmOLD  32819  cvrval2  33579  cvrnbtwn2  33580  cvrnbtwn3  33581  cvlsupr3  33649  cvrat4  33747  2at0mat0  33829  dalawlem13  34187  isltrn2N  34424  trlator0  34476  cdleme22b  34647  dochkrshp  35693  dochkrshp4  35696  lcfl6  35807  lclkrlem2x  35837  fphpd  36398  jm2.23  36581  sdrgacs  36790  isdomn3  36801  iunrelexp0  37013  ntrneineine1lem  37402  pm13.196a  37637  onfrALTlem5  37778  onfrALTlem3  37780  en3lpVD  38102  onfrALTlem5VD  38143  onfrALTlem3VD  38145  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  isosctrlem1ALT  38192  ndisj2  38243  cncfiooicclem1  38779  iblcncfioo  38870  stoweidlem28  38921  sge0iunmpt  39311  raaan2  39824  2reu4a  39838  afvfv0bi  39881  iccpartiltu  39960  iccpartlt  39962  icceuelpartlem  39973  lighneallem4  40065  oddprmALTV  40136  evenprm2  40161  cshword2  40300  pr1eqbg  40313  2f1fvneq  40322  2ffzoeq  40361  umgr2edg1  40438  nb3grprlem1  40608  1egrvtxdg0  40727  upgr1wlkwlk  40847  1wlkdlem4  40894  lfgriswlk  40897  pthdlem2  40974  wwlksnext  41099  clwlkclwwlklem2a4  41206  clwwisshclwwsn  41236  11wlkdlem4  41307  eupth2lem1  41386  eupth2lem3lem4  41399  frgr3vlem1  41443  frgr3vlem2  41444  3vfriswmgrlem  41447  4cycl2vnunb-av  41460  frgrncvvdeqlemB  41477  frgrregorufr  41490  av-frgrareg  41548  av-frgraregord013  41549  copisnmnd  41599  fdmdifeqresdif  41913  pgrpgt2nabl  41941  islindeps  42036  lincext1  42037  lindslinindsimp2lem5  42045  snlindsntor  42054  ldepslinc  42092  m1modmmod  42110  ssdifsn  42228