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

Definition df-ne 2627
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 2625 . 2  wff  A  =/= 
B
41, 2wceq 1437 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 187 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff setvar class
This definition is referenced by:  neii  2629  neir  2630  nne  2631  neneqd  2632  neqned  2634  exmidne  2636  exmidneOLD  2637  eqneqall  2638  nonconneOLD  2640  necon2bd  2646  necon1adOLD  2648  necon1bd  2649  necon3d  2655  necon2d  2657  necon1aiOLD  2663  necon1bi  2664  necon1i  2673  necon3abid  2677  necon1abidOLD  2680  necon1bbid  2681  necon4abidOLD  2683  necon2abidOLD  2686  necon2bbidOLD  2688  necon3bid  2689  necon3abii  2691  necon1abiiOLD  2694  necon1bbiiOLD  2696  necon3bii  2699  neeq1OLD  2713  neeq2OLD  2715  pm2.61iineOLD  2754  neor  2755  neanior  2756  neorian  2758  nfne  2763  nfned  2764  nabbi  2765  nabbiOLD  2766  dfpss2  3556  neq0  3778  ifnefalse  3927  snnzb  4067  raldifsni  4133  eqsn  4164  opthpr  4181  unissint  4283  iununi  4390  disji2  4413  opthneg  4701  frsn  4925  xpcan  5293  xpcan2  5294  xpima  5299  unixpid  5391  ord0eln0  5496  unizlim  5558  dff14a  6185  mpt2difsnif  6403  orduniorsuc  6671  dflim3  6688  tfindsg  6701  nn0suc  6731  findsg  6734  suppvalbr  6929  wfrlem16  7059  tz7.49  7170  oevn0  7225  php  7762  1sdom  7781  fimaxg  7824  fiint  7854  wemapsolem  8065  card2on  8069  brwdomn0  8084  domwdom  8089  rankxplim2  8350  rankxplim3  8351  carden2a  8399  dfackm  8594  fin23lem14  8761  fin1a2lem12  8839  axcc2lem  8864  ac6num  8907  zorn2lem4  8927  zorn2lem7  8930  brdom3  8954  iundom2g  8963  r1tskina  9206  1re  9641  ltlen  9734  uzm1  11189  xrnemnf  11419  xrnepnf  11420  ioo0  11661  ico0  11682  ioc0  11683  icc0  11684  elfznelfzo  12011  elfznelfzob  12012  injresinjlem  12021  fleqceilz  12078  fsuppmapnn0fiubex  12201  sq01  12391  hash1snb  12588  hashgt12el  12590  hashgt12el2  12591  hashfun  12604  hash2prde  12625  hash2prd  12627  hashge2el2dif  12630  swrdccatin1  12824  repswcshw  12896  cshw1  12906  xptrrel  13023  incexc2  13874  sqrt2irr  14279  divalglem8  14356  ndvdssub  14363  algcvgblem  14507  lcmcllem  14532  lcmfunsnlem2lem2  14583  lcmfunsnlem2  14584  isprm2lem  14602  isprm3  14604  isprm4  14605  ncoprmgcdne1b  14626  ramcl2lem  14925  ramcl2lemOLD  14926  cshwshashlem1  15029  cshwshash  15038  isnsgrp  16482  isnmnd  16491  sgrp2nmndlem3  16610  sgrp2rid2  16611  sgrp2nmndlem5  16614  symg2bas  16990  symgextf  17009  symgextfv  17010  odlem1  17126  gexlem1  17166  dprdfeq0  17590  isnirred  17863  isirred2  17864  drngmul0or  17931  drngmuleq0  17933  lvecvs0or  18266  lvecvscan  18269  isnzr2  18422  isdomn2  18458  cply1mul  18822  gsummoncoe1  18833  domnchr  19034  psgndiflemB  19099  dmatmul  19453  mulmarep1gsum1  19529  mulmarep1gsum2  19530  mdetdiag  19555  mdetunilem8  19575  mdetunilem9  19576  madurid  19600  mp2pm2mplem4  19764  fvmptnn04if  19804  fvmptnn04ifb  19806  elcls  20020  opnnei  20067  ist0-3  20292  ist1-2  20294  dfcon2  20365  cnconn  20368  pthaus  20584  xkohaus  20599  hausflim  20927  cldsubg  21056  bcth  22190  ioorinv  22405  ioorinvOLD  22410  tdeglem4  22886  fta1b  22995  plydivex  23118  plyexmo  23134  aalioulem3  23155  dvradcnv  23241  logtayllem  23469  logtayl  23470  cxpcl  23484  recxpcl  23485  logrec  23565  isosctrlem2  23613  efrlim  23760  muval2  23924  musum  23983  dchrelbas2  24028  dchrelbas4  24034  dchrfi  24046  dchrptlem3  24057  dchrsum2  24059  sumdchr2  24061  lgscllem  24094  2sqb  24169  dchrvmasumiflem2  24203  rpvmasum2  24213  padicabv  24331  padicabvf  24332  padicabvcxp  24333  tglowdim1i  24408  tgbtwnconn1  24480  colline  24554  colmid  24590  lmimid  24692  lmiisolem  24694  brbtwn2  24781  colinearalg  24786  axlowdimlem6  24823  axlowdimlem14  24831  axcontlem12  24851  usgra2edg1  24956  nbgranself  25007  nb3graprlem1  25024  uvtx01vtx  25065  wlkdvspthlem  25182  usgrcyclnl1  25213  usgrcyclnl2  25214  constr3trllem2  25224  wwlknext  25297  clwlkisclwwlklem2a4  25357  clwwisshclwwn  25381  clwlknclwlkdifs  25533  eupath2lem1  25550  frgra3vlem1  25573  frgra3vlem2  25574  3vfriswmgralem  25577  2pthfrgra  25584  4cycl2vnunb  25590  n4cyclfrgra  25591  frgrancvvdeqlemA  25610  frgrancvvdeqlemB  25611  frgrancvvdeqlemC  25612  frgraregorufr0  25625  frgraregorufr  25626  numclwwlk3lem  25681  frgrareg  25690  frgraregord013  25691  ismgmOLD  25893  nvmul0or  26118  nmogtmnf  26256  hvmul0or  26513  hvmulcan  26560  hvmulcan2  26561  hiidge0  26586  bcsiALT  26667  shne0i  26936  nonbooli  27139  nmopgtmnf  27356  unopbd  27503  nmcfnlbi  27540  nmopcoi  27583  chirredi  27882  mdsymlem5  27895  sumdmdlem2  27907  disji2f  28026  imadifxp  28051  aciunf1  28105  2sqcoprm  28246  sitgaddlemb  29009  sgn3da  29200  plymulx  29225  bnj1109  29386  bnj1542  29456  bnj1253  29614  subfacp1lem6  29696  cvmsdisj  29781  sltval2  30330  sltres  30338  nodenselem4  30358  nodenselem5  30359  nodenselem7  30361  nobndup  30374  nobnddown  30375  nofulllem5  30380  btwnconn1lem13  30651  lineunray  30699  rankeq1o  30723  elicc3  30758  nn0prpw  30764  ordtoplem  30880  icorempt2  31488  poimirlem1  31644  poimirlem14  31657  poimirlem16  31659  poimirlem19  31662  poimirlem23  31666  poimirlem25  31668  poimirlem26  31669  itg2addnclem3  31698  itgaddnclem2  31704  fdc  31777  prtlem90  32136  cvrval2  32548  cvrnbtwn2  32549  cvrnbtwn3  32550  cvlsupr3  32618  cvrat4  32716  2at0mat0  32798  dalawlem13  33156  isltrn2N  33393  trlator0  33445  cdleme22b  33616  dochkrshp  34662  dochkrshp4  34665  lcfl6  34776  lclkrlem2x  34806  fphpd  35367  jm2.23  35556  sdrgacs  35765  isdomn3  35779  iunrelexp0  35932  pm13.196a  36401  onfrALTlem5  36544  onfrALTlem3  36546  en3lpVD  36880  onfrALTlem5VD  36921  onfrALTlem3VD  36923  ax6e2ndeqVD  36945  ax6e2ndeqALT  36967  isosctrlem1ALT  36970  ndisj2  37029  cncfiooicclem1  37342  iblcncfioo  37423  stoweidlem28  37456  sge0iunmpt  37793  raaan2  37986  2reu4a  38000  afvfv0bi  38043  iccpartiltu  38125  iccpartlt  38127  icceuelpartlem  38138  oddprmALTV  38205  evenprm2  38231  cshword2  38367  pr1eqbg  38373  2f1fvneq  38383  2ffzoeq  38412  usg2edgneu  38481  copisnmnd  38566  fdmdifeqresdif  38882  pgrpgt2nabl  38910  islindeps  39005  lincext1  39006  lindslinindsimp2lem5  39014  snlindsntor  39023  ldepslinc  39061  m1modmmod  39084
  Copyright terms: Public domain W3C validator