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

Definition df-ne 2608
Description: Define inequality. (Contributed by NM, 5-Aug-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 2606 . 2  wff  A  =/= 
B
41, 2wceq 1654 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 178 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  neii  2610  neir  2611  nne  2612  exmidne  2614  nonconne  2615  neeq1  2616  neeq2  2617  neneqd  2624  necon3abii  2638  necon3bii  2640  necon3abid  2641  necon3bid  2643  necon3d  2646  necon1ai  2653  necon1i  2655  necon2bd  2660  necon2d  2661  necon1abii  2662  necon1bbii  2663  necon1abid  2664  necon1bbid  2665  necon2abid  2668  necon2bbid  2669  necon4abid  2675  necon1ad  2678  neor  2695  neanior  2696  neorian  2698  nfne  2702  nfned  2703  dfpss2  3421  neq0  3626  ifnefalse  3775  eqsn  3989  opthpr  4005  prnebg  4008  unissint  4103  iununi  4206  disji2  4230  ord0eln0  4670  unizlim  4733  orduniorsuc  4845  dflim3  4862  tfindsg  4875  nn0suc  4904  findsg  4907  frsn  4983  xpcan  5340  xpcan2  5341  xpima  5348  unixpid  5439  bropopvvv  6462  tz7.49  6738  oevn0  6795  php  7327  1sdom  7347  fimaxg  7390  fiint  7419  wemapso2lem  7555  card2on  7558  brwdomn0  7573  domwdom  7578  rankxplim2  7842  rankxplim3  7843  carden2a  7891  dfackm  8084  fin23lem14  8251  fin1a2lem12  8329  axcc2lem  8354  ac6num  8397  zorn2lem4  8417  zorn2lem7  8420  brdom3  8444  iundom2g  8453  r1tskina  8695  1re  9128  ltlen  9213  uzm1  10554  xrnemnf  10756  xrnepnf  10757  ioo0  10979  ico0  11000  ioc0  11001  icc0  11002  elfznelfzo  11230  elfznelfzob  11231  injresinjlem  11237  sq01  11539  hash1snb  11719  hashgt12el  11720  hashgt12el2  11721  hash2prde  11726  hashfun  11738  incexc2  12656  sqr2irr  12886  divalglem8  12958  ndvdssub  12965  algcvgblem  13106  isprm2lem  13124  isprm3  13126  isprm4  13127  ramcl2lem  13415  odlem1  15211  gexlem1  15251  dprdfeq0  15618  isnirred  15843  isirred2  15844  drngmul0or  15894  drngmuleq0  15896  lvecvs0or  16218  lvecvscan  16221  isnzr2  16372  isdomn2  16397  domnchr  16851  elcls  17175  opnnei  17222  ist0-3  17447  ist1-2  17449  dfcon2  17520  cnconn  17523  pthaus  17708  xkohaus  17723  hausflim  18051  cldsubg  18178  bcth  19320  ioorinv  19506  tdeglem4  20021  fta1b  20130  plydivex  20252  plyexmo  20268  aalioulem3  20289  dvradcnv  20375  logtayllem  20588  logtayl  20589  cxpcl  20603  recxpcl  20604  logrec  20699  isosctrlem2  20701  efrlim  20846  muval2  20955  musum  21014  dchrelbas2  21059  dchrelbas4  21065  dchrfi  21077  dchrptlem3  21088  dchrsum2  21090  sumdchr2  21092  lgscllem  21125  2sqb  21200  dchrvmasumiflem2  21234  rpvmasum2  21244  padicabv  21362  padicabvf  21363  padicabvcxp  21364  usgra2edg  21440  usgra2edg1  21441  nbgranself  21484  nb3graprlem1  21498  uvtx01vtx  21539  wlkdvspthlem  21645  usgrcyclnl1  21665  usgrcyclnl2  21666  constr3trllem2  21676  eupath2lem1  21737  ismgm  21946  vcoprne  22096  nvmul0or  22171  nmogtmnf  22309  hvmul0or  22565  hvmulcan  22612  hvmulcan2  22613  hiidge0  22638  bcsiALT  22719  norm1exi  22790  shne0i  22988  nonbooli  23191  nmopgtmnf  23409  unopbd  23556  nmcfnlbi  23593  nmopcoi  23636  largei  23808  chirredi  23935  mdsymlem5  23948  sumdmdlem2  23960  disji2f  24054  iundisj2f  24065  imadifxp  24073  iundisj2fi  24188  ind1a  24453  ballotlemii  24796  subfacp1lem6  24906  cvmsdisj  24992  cvmscld  24995  pm2.61iine  25221  snnzb  25437  dfrdg2  25458  wfrlem16  25588  sltval2  25646  nosgnn0  25648  nosgnn0i  25649  sltintdifex  25653  sltres  25654  sltsolem1  25658  nodenselem4  25674  nodenselem5  25675  nodenselem7  25677  nobndup  25690  nobnddown  25691  nofulllem5  25696  dfrdg4  25830  brbtwn2  25879  colinearalg  25884  axlowdimlem6  25921  axlowdimlem13  25928  axlowdimlem14  25929  axlowdim1  25933  axcontlem12  25949  btwnconn1lem13  26068  lineunray  26116  rankeq1o  26147  ordtoplem  26220  itg2addnclem3  26300  itgaddnclem2  26306  elicc3  26362  nn0prpw  26368  fdc  26491  prtlem90  26818  raldifsni  26846  cmpfiiin  26863  0dioph  26949  fphpd  26989  jm2.23  27179  wepwsolem  27228  uvcvv0  27328  sdrgacs  27598  isdomn3  27612  pm13.196a  27703  refsum2cnlem1  27796  fmul01lt1lem1  27802  stoweidlem14  27851  stoweidlem28  27865  stoweidlem55  27892  stoweid  27900  raaan2  28041  2reu4a  28055  afvfv0bi  28104  eqneqall  28162  pr1eqbg  28168  2f1fvneq  28193  dff14a  28194  2ffzoeq  28261  euhash1  28288  swrdccatin1  28337  2cshwmod  28389  cshw1  28407  cshwssizelem1a  28411  cshwssizelem2  28413  cshwssizelem3  28414  cshwssize  28422  frgra3vlem1  28562  frgra3vlem2  28563  3vfriswmgralem  28566  2pthfrgra  28573  4cycl2vnunb  28579  n4cyclfrgra  28580  frgrancvvdeqlemA  28598  frgrancvvdeqlemB  28599  frgrancvvdeqlemC  28600  frgrawopreglem3  28607  frgrawopreglem4  28608  frgraregorufr0  28613  frgraregorufr  28614  usg2spot2nb  28626  sgnn  28696  onfrALTlem5  28800  onfrALTlem3  28802  en3lpVD  29131  onfrALTlem5VD  29171  onfrALTlem3VD  29173  a9e2ndeqVD  29195  a9e2ndeqALT  29217  isosctrlem1ALT  29220  bnj1109  29331  bnj1542  29402  bnj1253  29560  cvrval2  30246  cvrnbtwn2  30247  cvrnbtwn3  30248  cvlsupr3  30316  hlrelat5N  30372  cvrat4  30414  2at0mat0  30496  dalawlem13  30854  isltrn2N  31091  trlator0  31142  cdleme22b  31312  dochkrshp  32358  dochkrshp4  32361  lcfl6  32472  lclkrlem2x  32502
  Copyright terms: Public domain W3C validator