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

Definition df-ne 2635
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 2633 . 2  wff  A  =/= 
B
41, 2wceq 1455 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 189 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff setvar class
This definition is referenced by:  neii  2637  neir  2638  nne  2639  neneqd  2640  neqned  2642  exmidne  2645  eqneqall  2646  nonconneOLD  2648  necon2bd  2652  necon1bd  2654  necon3d  2657  necon2d  2659  necon1bi  2664  necon1i  2669  necon3abid  2672  necon1bbid  2675  necon3bid  2680  necon3abii  2682  necon3bii  2688  neor  2727  neanior  2728  neorian  2730  nfne  2735  nfned  2736  nabbi  2737  dfpss2  3530  neq0  3754  ifnefalse  3905  snnzb  4049  raldifsni  4115  eqsn  4146  opthpr  4166  unissint  4273  iununi  4382  disji2  4405  opthneg  4698  frsn  4927  xpcan  5295  xpcan2  5296  xpima  5301  unixpid  5394  ord0eln0  5500  unizlim  5562  dff14a  6200  mpt2difsnif  6421  orduniorsuc  6689  dflim3  6706  tfindsg  6719  nn0suc  6749  findsg  6752  suppvalbr  6950  wfrlem16  7082  tz7.49  7193  oevn0  7248  php  7787  1sdom  7806  fimaxg  7849  fiint  7879  wemapsolem  8096  card2on  8100  brwdomn0  8115  domwdom  8120  rankxplim2  8382  rankxplim3  8383  carden2a  8431  dfackm  8627  fin23lem14  8794  fin1a2lem12  8872  axcc2lem  8897  ac6num  8940  zorn2lem4  8960  zorn2lem7  8963  brdom3  8987  iundom2g  8996  r1tskina  9238  1re  9673  ltlen  9766  uzm1  11223  xrnemnf  11453  xrnepnf  11454  ioo0  11695  ico0  11716  ioc0  11717  icc0  11718  elfznelfzo  12051  elfznelfzob  12052  injresinjlem  12062  fleqceilz  12119  fsuppmapnn0fiubex  12242  sq01  12432  hash1snb  12632  hashgt12el  12634  hashgt12el2  12635  hashfun  12648  hash2prde  12670  hashge2el2dif  12676  swrdccatin1  12882  repswcshw  12954  cshw1  12964  xptrrel  13099  incexc2  13951  sqrt2irr  14356  divalglem8  14435  ndvdssub  14443  algcvgblem  14591  lcmcllem  14616  lcmfunsnlem2lem2  14667  lcmfunsnlem2  14668  isprm2lem  14686  isprm3  14688  isprm4  14689  ncoprmgcdne1b  14710  ramcl2lem  15017  ramcl2lemOLD  15018  cshwshashlem1  15121  cshwshash  15130  isnsgrp  16586  isnmnd  16595  sgrp2nmndlem3  16714  sgrp2rid2  16715  sgrp2nmndlem5  16718  symg2bas  17094  symgextf  17113  symgextfv  17114  odlem1  17236  odlem1OLD  17239  gexlem1  17283  gexlem1OLD  17285  dprdfeq0  17710  isnirred  17983  isirred2  17984  drngmul0or  18051  drngmuleq0  18053  lvecvs0or  18386  lvecvscan  18389  isnzr2  18542  isdomn2  18578  cply1mul  18942  gsummoncoe1  18953  domnchr  19158  psgndiflemB  19223  dmatmul  19577  mulmarep1gsum1  19653  mulmarep1gsum2  19654  mdetdiag  19679  mdetunilem8  19699  mdetunilem9  19700  madurid  19724  mp2pm2mplem4  19888  fvmptnn04if  19928  fvmptnn04ifb  19930  elcls  20144  opnnei  20191  ist0-3  20416  ist1-2  20418  dfcon2  20489  cnconn  20492  pthaus  20708  xkohaus  20723  hausflim  21051  cldsubg  21180  bcth  22352  ioorinv  22584  ioorinvOLD  22589  tdeglem4  23065  fta1b  23176  plydivex  23306  plyexmo  23322  aalioulem3  23346  dvradcnv  23432  logtayllem  23660  logtayl  23661  cxpcl  23675  recxpcl  23676  logrec  23756  isosctrlem2  23804  efrlim  23951  muval2  24117  musum  24176  dchrelbas2  24221  dchrelbas4  24227  dchrfi  24239  dchrptlem3  24250  dchrsum2  24252  sumdchr2  24254  lgscllem  24287  2sqb  24362  dchrvmasumiflem2  24396  rpvmasum2  24406  padicabv  24524  padicabvf  24525  padicabvcxp  24526  tglowdim1i  24601  tgbtwnconn1  24676  colline  24750  colmid  24789  lmimid  24892  lmiisolem  24894  brbtwn2  24991  colinearalg  24996  axlowdimlem6  25033  axlowdimlem14  25041  axcontlem12  25061  usgra2edg1  25166  nbgranself  25218  nb3graprlem1  25235  uvtx01vtx  25276  wlkdvspthlem  25393  usgrcyclnl1  25424  usgrcyclnl2  25425  constr3trllem2  25435  wwlknext  25508  clwlkisclwwlklem2a4  25568  clwwisshclwwn  25592  clwlknclwlkdifs  25744  eupath2lem1  25761  frgra3vlem1  25784  frgra3vlem2  25785  3vfriswmgralem  25788  2pthfrgra  25795  4cycl2vnunb  25801  n4cyclfrgra  25802  frgrancvvdeqlemA  25821  frgrancvvdeqlemB  25822  frgrancvvdeqlemC  25823  frgraregorufr0  25836  frgraregorufr  25837  numclwwlk3lem  25892  frgrareg  25901  frgraregord013  25902  ismgmOLD  26104  nvmul0or  26329  nmogtmnf  26467  hvmul0or  26734  hvmulcan  26781  hvmulcan2  26782  hiidge0  26807  bcsiALT  26888  shne0i  27157  nonbooli  27360  nmopgtmnf  27577  unopbd  27724  nmcfnlbi  27761  nmopcoi  27804  chirredi  28103  mdsymlem5  28116  sumdmdlem2  28128  disji2f  28241  imadifxp  28265  aciunf1  28317  2sqcoprm  28460  sitgaddlemb  29231  sgn3da  29462  plymulx  29487  bnj1109  29648  bnj1542  29718  bnj1253  29876  subfacp1lem6  29958  cvmsdisj  30043  sltval2  30593  sltres  30601  noseponlem  30605  nosepon  30606  nodenselem4  30623  nodenselem5  30624  nodenselem7  30626  nobndup  30639  nobnddown  30640  nofulllem5  30645  btwnconn1lem13  30916  lineunray  30964  rankeq1o  30988  elicc3  31023  nn0prpw  31029  ordtoplem  31145  icorempt2  31800  poimirlem1  31987  poimirlem14  32000  poimirlem16  32002  poimirlem19  32005  poimirlem23  32009  poimirlem25  32011  poimirlem26  32012  itg2addnclem3  32041  itgaddnclem2  32047  fdc  32120  prtlem90  32477  cvrval2  32886  cvrnbtwn2  32887  cvrnbtwn3  32888  cvlsupr3  32956  cvrat4  33054  2at0mat0  33136  dalawlem13  33494  isltrn2N  33731  trlator0  33783  cdleme22b  33954  dochkrshp  35000  dochkrshp4  35003  lcfl6  35114  lclkrlem2x  35144  fphpd  35705  jm2.23  35897  sdrgacs  36113  isdomn3  36127  iunrelexp0  36340  pm13.196a  36810  onfrALTlem5  36953  onfrALTlem3  36955  en3lpVD  37282  onfrALTlem5VD  37323  onfrALTlem3VD  37325  ax6e2ndeqVD  37347  ax6e2ndeqALT  37369  isosctrlem1ALT  37372  ndisj2  37428  cncfiooicclem1  37857  iblcncfioo  37941  stoweidlem28  37989  sge0iunmpt  38363  raaan2  38731  2reu4a  38745  afvfv0bi  38789  iccpartiltu  38871  iccpartlt  38873  icceuelpartlem  38884  oddprmALTV  38951  evenprm2  38977  cshword2  39115  pr1eqbg  39128  n0snor2el  39133  2f1fvneq  39150  fundmge2nop  39164  2ffzoeq  39202  incistruhgr  39314  usgr2edg1  39438  nb3grprlem1  39600  upgr1wlkwlk  39796  lfgriswlk  39819  1wlkdlem4  39824  pthdlem2  39890  11wlkdlem4  39951  usg2edgneu  40093  copisnmnd  40178  fdmdifeqresdif  40492  pgrpgt2nabl  40520  islindeps  40615  lincext1  40616  lindslinindsimp2lem5  40624  snlindsntor  40633  ldepslinc  40671  m1modmmod  40693
  Copyright terms: Public domain W3C validator