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

Definition df-ne 2616
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 2614 . 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  2618  neir  2619  nne  2620  neneqd  2621  neqned  2623  exmidne  2625  exmidneOLD  2626  eqneqall  2627  nonconneOLD  2629  necon2bd  2635  necon1adOLD  2637  necon1bd  2638  necon3d  2644  necon2d  2646  necon1aiOLD  2652  necon1bi  2653  necon1i  2662  necon3abid  2666  necon1abidOLD  2669  necon1bbid  2670  necon4abidOLD  2672  necon2abidOLD  2675  necon2bbidOLD  2677  necon3bid  2678  necon3abii  2680  necon1abiiOLD  2683  necon1bbiiOLD  2685  necon3bii  2688  neeq1OLD  2702  neeq2OLD  2704  pm2.61iineOLD  2743  neor  2744  neanior  2745  neorian  2747  nfne  2752  nfned  2753  nabbi  2754  nabbiOLD  2755  dfpss2  3550  neq0  3772  ifnefalse  3923  snnzb  4064  raldifsni  4130  eqsn  4161  opthpr  4178  unissint  4280  iununi  4387  disji2  4410  opthneg  4700  frsn  4924  xpcan  5292  xpcan2  5293  xpima  5298  unixpid  5390  ord0eln0  5496  unizlim  5558  dff14a  6185  mpt2difsnif  6403  orduniorsuc  6671  dflim3  6688  tfindsg  6701  nn0suc  6731  findsg  6734  suppvalbr  6929  wfrlem16  7062  tz7.49  7173  oevn0  7228  php  7765  1sdom  7784  fimaxg  7827  fiint  7857  wemapsolem  8074  card2on  8078  brwdomn0  8093  domwdom  8098  rankxplim2  8359  rankxplim3  8360  carden2a  8408  dfackm  8603  fin23lem14  8770  fin1a2lem12  8848  axcc2lem  8873  ac6num  8916  zorn2lem4  8936  zorn2lem7  8939  brdom3  8963  iundom2g  8972  r1tskina  9214  1re  9649  ltlen  9742  uzm1  11196  xrnemnf  11426  xrnepnf  11427  ioo0  11668  ico0  11689  ioc0  11690  icc0  11691  elfznelfzo  12020  elfznelfzob  12021  injresinjlem  12030  fleqceilz  12087  fsuppmapnn0fiubex  12210  sq01  12400  hash1snb  12597  hashgt12el  12599  hashgt12el2  12600  hashfun  12613  hash2prde  12635  hashge2el2dif  12641  swrdccatin1  12841  repswcshw  12913  cshw1  12923  xptrrel  13044  incexc2  13895  sqrt2irr  14300  divalglem8  14379  ndvdssub  14387  algcvgblem  14535  lcmcllem  14560  lcmfunsnlem2lem2  14611  lcmfunsnlem2  14612  isprm2lem  14630  isprm3  14632  isprm4  14633  ncoprmgcdne1b  14654  ramcl2lem  14961  ramcl2lemOLD  14962  cshwshashlem1  15065  cshwshash  15074  isnsgrp  16530  isnmnd  16539  sgrp2nmndlem3  16658  sgrp2rid2  16659  sgrp2nmndlem5  16662  symg2bas  17038  symgextf  17057  symgextfv  17058  odlem1  17180  odlem1OLD  17183  gexlem1  17227  gexlem1OLD  17229  dprdfeq0  17654  isnirred  17927  isirred2  17928  drngmul0or  17995  drngmuleq0  17997  lvecvs0or  18330  lvecvscan  18333  isnzr2  18486  isdomn2  18522  cply1mul  18886  gsummoncoe1  18897  domnchr  19101  psgndiflemB  19166  dmatmul  19520  mulmarep1gsum1  19596  mulmarep1gsum2  19597  mdetdiag  19622  mdetunilem8  19642  mdetunilem9  19643  madurid  19667  mp2pm2mplem4  19831  fvmptnn04if  19871  fvmptnn04ifb  19873  elcls  20087  opnnei  20134  ist0-3  20359  ist1-2  20361  dfcon2  20432  cnconn  20435  pthaus  20651  xkohaus  20666  hausflim  20994  cldsubg  21123  bcth  22295  ioorinv  22526  ioorinvOLD  22531  tdeglem4  23007  fta1b  23118  plydivex  23248  plyexmo  23264  aalioulem3  23288  dvradcnv  23374  logtayllem  23602  logtayl  23603  cxpcl  23617  recxpcl  23618  logrec  23698  isosctrlem2  23746  efrlim  23893  muval2  24059  musum  24118  dchrelbas2  24163  dchrelbas4  24169  dchrfi  24181  dchrptlem3  24192  dchrsum2  24194  sumdchr2  24196  lgscllem  24229  2sqb  24304  dchrvmasumiflem2  24338  rpvmasum2  24348  padicabv  24466  padicabvf  24467  padicabvcxp  24468  tglowdim1i  24543  tgbtwnconn1  24618  colline  24692  colmid  24731  lmimid  24834  lmiisolem  24836  brbtwn2  24933  colinearalg  24938  axlowdimlem6  24975  axlowdimlem14  24983  axcontlem12  25003  usgra2edg1  25108  nbgranself  25160  nb3graprlem1  25177  uvtx01vtx  25218  wlkdvspthlem  25335  usgrcyclnl1  25366  usgrcyclnl2  25367  constr3trllem2  25377  wwlknext  25450  clwlkisclwwlklem2a4  25510  clwwisshclwwn  25534  clwlknclwlkdifs  25686  eupath2lem1  25703  frgra3vlem1  25726  frgra3vlem2  25727  3vfriswmgralem  25730  2pthfrgra  25737  4cycl2vnunb  25743  n4cyclfrgra  25744  frgrancvvdeqlemA  25763  frgrancvvdeqlemB  25764  frgrancvvdeqlemC  25765  frgraregorufr0  25778  frgraregorufr  25779  numclwwlk3lem  25834  frgrareg  25843  frgraregord013  25844  ismgmOLD  26046  nvmul0or  26271  nmogtmnf  26409  hvmul0or  26676  hvmulcan  26723  hvmulcan2  26724  hiidge0  26749  bcsiALT  26830  shne0i  27099  nonbooli  27302  nmopgtmnf  27519  unopbd  27666  nmcfnlbi  27703  nmopcoi  27746  chirredi  28045  mdsymlem5  28058  sumdmdlem2  28070  disji2f  28189  imadifxp  28214  aciunf1  28267  2sqcoprm  28415  sitgaddlemb  29189  sgn3da  29420  plymulx  29445  bnj1109  29606  bnj1542  29676  bnj1253  29834  subfacp1lem6  29916  cvmsdisj  30001  sltval2  30550  sltres  30558  nodenselem4  30578  nodenselem5  30579  nodenselem7  30581  nobndup  30594  nobnddown  30595  nofulllem5  30600  btwnconn1lem13  30871  lineunray  30919  rankeq1o  30943  elicc3  30978  nn0prpw  30984  ordtoplem  31100  icorempt2  31718  poimirlem1  31905  poimirlem14  31918  poimirlem16  31920  poimirlem19  31923  poimirlem23  31927  poimirlem25  31929  poimirlem26  31930  itg2addnclem3  31959  itgaddnclem2  31965  fdc  32038  prtlem90  32397  cvrval2  32809  cvrnbtwn2  32810  cvrnbtwn3  32811  cvlsupr3  32879  cvrat4  32977  2at0mat0  33059  dalawlem13  33417  isltrn2N  33654  trlator0  33706  cdleme22b  33877  dochkrshp  34923  dochkrshp4  34926  lcfl6  35037  lclkrlem2x  35067  fphpd  35628  jm2.23  35821  sdrgacs  36037  isdomn3  36051  iunrelexp0  36264  pm13.196a  36735  onfrALTlem5  36878  onfrALTlem3  36880  en3lpVD  37214  onfrALTlem5VD  37255  onfrALTlem3VD  37257  ax6e2ndeqVD  37279  ax6e2ndeqALT  37301  isosctrlem1ALT  37304  ndisj2  37362  cncfiooicclem1  37711  iblcncfioo  37795  stoweidlem28  37828  sge0iunmpt  38168  raaan2  38467  2reu4a  38481  afvfv0bi  38524  iccpartiltu  38606  iccpartlt  38608  icceuelpartlem  38619  oddprmALTV  38686  evenprm2  38712  cshword2  38848  pr1eqbg  38857  n0snor2el  38862  2f1fvneq  38877  fundmge2nop  38889  2ffzoeq  38918  incistruhgr  39001  usgr2edg1  39076  nb3grprlem1  39214  usg2edgneu  39344  copisnmnd  39429  fdmdifeqresdif  39745  pgrpgt2nabl  39773  islindeps  39868  lincext1  39869  lindslinindsimp2lem5  39877  snlindsntor  39886  ldepslinc  39924  m1modmmod  39946
  Copyright terms: Public domain W3C validator