MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ne Structured version   Unicode version

Definition df-ne 2579
Description: Define inequality. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
df-ne  |-  ( A  =/=  B  <->  -.  A  =  B )

Detailed syntax breakdown of Definition df-ne
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wne 2577 . 2  wff  A  =/= 
B
41, 2wceq 1399 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 184 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff setvar class
This definition is referenced by:  neii  2581  neir  2582  nne  2583  neneqd  2584  neqned  2585  exmidne  2587  exmidneOLD  2588  eqneqall  2589  nonconneOLD  2591  necon2bd  2597  necon1adOLD  2599  necon1bd  2600  necon3d  2606  necon2d  2608  necon1aiOLD  2614  necon1bi  2615  necon1i  2624  necon3abid  2628  necon1abidOLD  2631  necon1bbid  2632  necon4abidOLD  2634  necon2abidOLD  2637  necon2bbidOLD  2639  necon3bid  2640  necon3abii  2642  necon1abiiOLD  2645  necon1bbiiOLD  2647  necon3bii  2650  neeq1OLD  2664  neeq2OLD  2666  pm2.61iineOLD  2705  neor  2706  neanior  2707  neorian  2709  nfne  2713  nfned  2714  nabbi  2715  nabbiOLD  2716  dfpss2  3503  neq0  3722  ifnefalse  3869  snnzb  4008  raldifsni  4074  eqsn  4105  opthpr  4122  unissint  4224  iununi  4331  disji2  4354  opthneg  4641  ord0eln0  4846  unizlim  4908  frsn  4984  xpcan  5353  xpcan2  5354  xpima  5359  unixpid  5451  dff14a  6078  mpt2difsnif  6294  orduniorsuc  6564  dflim3  6581  tfindsg  6594  nn0suc  6623  findsg  6626  suppvalbr  6821  tz7.49  7028  oevn0  7083  php  7620  1sdom  7639  fimaxg  7682  fiint  7712  wemapsolem  7890  card2on  7895  brwdomn0  7910  domwdom  7915  rankxplim2  8211  rankxplim3  8212  carden2a  8260  dfackm  8459  fin23lem14  8626  fin1a2lem12  8704  axcc2lem  8729  ac6num  8772  zorn2lem4  8792  zorn2lem7  8795  brdom3  8819  iundom2g  8828  r1tskina  9071  1re  9506  ltlen  9597  uzm1  11031  xrnemnf  11249  xrnepnf  11250  ioo0  11475  ico0  11496  ioc0  11497  icc0  11498  elfznelfzo  11814  elfznelfzob  11815  injresinjlem  11824  fleqceilz  11881  fsuppmapnn0fiubex  12001  sq01  12190  hash1snb  12383  hashgt12el  12385  hashgt12el2  12386  hashfun  12399  hash2prde  12420  hash2prd  12422  hashge2el2dif  12425  swrdccatin1  12619  repswcshw  12691  cshw1  12701  xptrrel  12818  incexc2  13652  sqrt2irr  13984  divalglem8  14060  ndvdssub  14067  algcvgblem  14208  isprm2lem  14226  isprm3  14228  isprm4  14229  ramcl2lem  14529  cshwshashlem1  14582  cshwshash  14591  isnsgrp  16032  isnmnd  16041  sgrp2nmndlem3  16160  sgrp2rid2  16161  sgrp2nmndlem5  16164  symg2bas  16540  symgextf  16559  symgextfv  16560  odlem1  16676  gexlem1  16716  dprdfeq0  17175  dprdfeq0OLD  17182  isnirred  17462  isirred2  17463  drngmul0or  17530  drngmuleq0  17532  lvecvs0or  17867  lvecvscan  17870  isnzr2  18024  isdomn2  18061  cply1mul  18448  gsummoncoe1  18459  domnchr  18662  psgndiflemB  18727  dmatmul  19084  mulmarep1gsum1  19160  mulmarep1gsum2  19161  mdetdiag  19186  mdetunilem8  19206  mdetunilem9  19207  madurid  19231  mp2pm2mplem4  19395  fvmptnn04if  19435  fvmptnn04ifb  19437  elcls  19660  opnnei  19707  ist0-3  19932  ist1-2  19934  dfcon2  20005  cnconn  20008  pthaus  20224  xkohaus  20239  hausflim  20567  cldsubg  20694  bcth  21853  ioorinv  22070  tdeglem4  22543  fta1b  22655  plydivex  22778  plyexmo  22794  aalioulem3  22815  dvradcnv  22901  logtayllem  23127  logtayl  23128  cxpcl  23142  recxpcl  23143  logrec  23221  isosctrlem2  23269  efrlim  23416  muval2  23525  musum  23584  dchrelbas2  23629  dchrelbas4  23635  dchrfi  23647  dchrptlem3  23658  dchrsum2  23660  sumdchr2  23662  lgscllem  23695  2sqb  23770  dchrvmasumiflem2  23804  rpvmasum2  23814  padicabv  23932  padicabvf  23933  padicabvcxp  23934  tglowdim1i  24012  tgbtwnconn1  24082  colline  24150  colmid  24185  lmimid  24279  lmiisolem  24281  brbtwn2  24329  colinearalg  24334  axlowdimlem6  24371  axlowdimlem14  24379  axcontlem12  24399  usgra2edg1  24504  nbgranself  24555  nb3graprlem1  24572  uvtx01vtx  24613  wlkdvspthlem  24730  usgrcyclnl1  24761  usgrcyclnl2  24762  constr3trllem2  24772  wwlknext  24845  clwlkisclwwlklem2a4  24905  clwwisshclwwn  24929  clwlknclwlkdifs  25081  eupath2lem1  25098  frgra3vlem1  25121  frgra3vlem2  25122  3vfriswmgralem  25125  2pthfrgra  25132  4cycl2vnunb  25138  n4cyclfrgra  25139  frgrancvvdeqlemA  25158  frgrancvvdeqlemB  25159  frgrancvvdeqlemC  25160  frgraregorufr0  25173  frgraregorufr  25174  numclwwlk3lem  25229  frgrareg  25238  frgraregord013  25239  ismgmOLD  25439  nvmul0or  25664  nmogtmnf  25802  hvmul0or  26059  hvmulcan  26106  hvmulcan2  26107  hiidge0  26132  bcsiALT  26213  shne0i  26483  nonbooli  26686  nmopgtmnf  26903  unopbd  27050  nmcfnlbi  27087  nmopcoi  27130  chirredi  27429  mdsymlem5  27442  sumdmdlem2  27454  disji2f  27567  imadifxp  27591  aciunf1  27649  2sqcoprm  27788  sgn3da  28663  plymulx  28688  subfacp1lem6  28818  cvmsdisj  28904  wfrlem16  29523  sltval2  29581  sltres  29589  nodenselem4  29609  nodenselem5  29610  nodenselem7  29612  nobndup  29625  nobnddown  29626  nofulllem5  29631  btwnconn1lem13  29902  lineunray  29950  rankeq1o  29981  ordtoplem  30053  itg2addnclem3  30234  itgaddnclem2  30240  elicc3  30301  nn0prpw  30307  fdc  30404  prtlem90  30764  fphpd  30915  jm2.23  31104  sdrgacs  31318  isdomn3  31332  lcmcllem  31370  pm13.196a  31489  cncfiooicclem1  31862  iblcncfioo  31943  stoweidlem28  31976  raaan2  32346  2reu4a  32360  afvfv0bi  32403  oddprmALTV  32529  cshword2  32612  pr1eqbg  32618  2f1fvneq  32628  2ffzoeq  32661  usg2edgneu  32730  copisnmnd  32815  fdmdifeqresdif  33131  pgrpgt2nabl  33159  islindeps  33254  lincext1  33255  lindslinindsimp2lem5  33263  snlindsntor  33272  ldepslinc  33310  m1modmmod  33334  onfrALTlem5  33654  onfrALTlem3  33656  en3lpVD  33991  onfrALTlem5VD  34032  onfrALTlem3VD  34034  ax6e2ndeqVD  34056  ax6e2ndeqALT  34078  isosctrlem1ALT  34081  bnj1109  34192  bnj1542  34262  bnj1253  34420  cvrval2  35412  cvrnbtwn2  35413  cvrnbtwn3  35414  cvlsupr3  35482  cvrat4  35580  2at0mat0  35662  dalawlem13  36020  isltrn2N  36257  trlator0  36309  cdleme22b  36480  dochkrshp  37526  dochkrshp4  37529  lcfl6  37640  lclkrlem2x  37670  iunrelexp0  38242
  Copyright terms: Public domain W3C validator