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

Definition df-ne 2573
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 2571 . 2  wff  A  =/= 
B
41, 2wceq 1649 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 177 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  nne  2575  exmidne  2577  nonconne  2578  neeq1  2579  neeq2  2580  neneqd  2587  necon3abii  2601  necon3bii  2603  necon3abid  2604  necon3bid  2606  necon3d  2609  necon1ai  2613  necon1i  2615  necon2bd  2620  necon2d  2621  necon1abii  2622  necon1bbii  2623  necon1abid  2624  necon1bbid  2625  necon2abid  2628  necon2bbid  2629  necon4abid  2635  necon1ad  2638  neor  2655  neanior  2656  neorian  2658  nemtbir  2659  nfne  2662  nfned  2663  dfpss2  3396  neq0  3602  ifnefalse  3711  eqsn  3924  snsssn  3931  opthpr  3940  prnebg  3943  unissint  4038  iununi  4139  disji2  4163  ord0eln0  4599  nsuceq0  4625  unizlim  4661  orduniorsuc  4773  dflim3  4790  tfindsg  4803  nn0suc  4832  findsg  4835  frsn  4911  xpcan  5268  xpcan2  5269  xpima  5276  unixpid  5367  0neqopab  6082  bropopvvv  6389  tz7.49  6665  oevn0  6722  2dom  7142  map2xp  7240  php  7254  1sdom  7274  fimaxg  7317  fiint  7346  wemapso2lem  7479  card2on  7482  brwdomn0  7497  domwdom  7502  rankxplim2  7764  rankxplim3  7765  carden2a  7813  pm54.43lem  7846  dfackm  8006  fin23lem14  8173  fin1a2lem12  8251  axcc2lem  8276  ac6num  8319  zorn2lem4  8339  zorn2lem7  8342  brdom3  8366  iundom2g  8375  canthp1lem2  8488  r1tskina  8617  ax1ne0  8995  1re  9050  ltlen  9135  ine0  9429  recgt0ii  9876  inelr  9950  nnunb  10177  uzm1  10476  xrnemnf  10678  xrnepnf  10679  xrltnr  10680  pnfnlt  10685  nltmnf  10686  xrltlen  10699  ioo0  10901  ico0  10922  ioc0  10923  icc0  10924  fzm1  11086  elfznelfzo  11151  elfznelfzob  11152  injresinjlem  11158  sq01  11460  hash1snb  11640  hashgt12el  11641  hashgt12el2  11642  hash2prde  11647  hashfun  11659  incexc2  12577  sqr2irr  12807  divalglem8  12879  ndvdssub  12886  algcvgblem  13027  isprm2lem  13045  isprm3  13047  isprm4  13048  ramcl2lem  13336  xpsfrnel2  13749  setcepi  14202  odlem1  15132  gexlem1  15172  dprdfeq0  15539  isnirred  15764  isirred2  15765  drngmul0or  15815  drngmuleq0  15817  lvecvs0or  16139  lvecvscan  16142  lspsncv0  16177  isnzr2  16293  isdomn2  16318  domnchr  16772  elcls  17096  opnnei  17143  ist0-3  17367  ist1-2  17369  dfcon2  17439  cnconn  17442  pthaus  17627  xkohaus  17642  trfbas  17833  fbunfip  17858  trfil2  17876  hausflim  17970  cldsubg  18097  bcth  19239  iundisj2  19400  ioorinv  19425  tdeglem4  19940  fta1b  20049  plydivex  20171  vieta1lem2  20185  plyexmo  20187  aalioulem3  20208  dvradcnv  20294  sinhalfpilem  20331  coseq1  20387  logtayllem  20507  logtayl  20508  cxpcl  20522  recxpcl  20523  logrec  20618  isosctrlem2  20620  efrlim  20765  muval2  20874  musum  20933  dchrelbas2  20978  dchrelbas4  20984  dchrfi  20996  dchrptlem3  21007  dchrsum2  21009  sumdchr2  21011  lgscllem  21044  2sqb  21119  dchrvmasumiflem2  21153  rpvmasum2  21163  padicabv  21281  padicabvf  21282  padicabvcxp  21283  usgraedgprv  21353  usgra2edg  21359  usgra2edg1  21360  nbgranself  21403  nb3graprlem1  21417  uvtx01vtx  21458  2trllemA  21507  wlkntrllem3  21518  2pthon  21559  2pthon3v  21561  wlkdvspthlem  21564  usgrcyclnl1  21584  usgrcyclnl2  21585  constr3trllem2  21595  4cycl4dv  21611  eupath2lem1  21656  ismgm  21865  vcoprne  22015  nvmul0or  22090  nmogtmnf  22228  hvmul0or  22484  hvmulcan  22531  hvmulcan2  22532  hiidge0  22557  bcsiALT  22638  norm1exi  22709  shne0i  22907  nonbooli  23110  nmopgtmnf  23328  unopbd  23475  nmcfnlbi  23512  nmopcoi  23555  largei  23727  chirredi  23854  mdsymlem5  23867  sumdmdlem2  23879  disji2f  23976  iundisj2f  23987  imadifxp  23995  iundisj2fi  24110  ind1a  24375  ballotlemii  24718  subfacp1lem6  24828  cvmsdisj  24914  cvmscld  24917  pm2.61iine  25143  dfrdg2  25370  wfrlem16  25489  sltval2  25528  nosgnn0  25530  nosgnn0i  25531  sltintdifex  25535  sltres  25536  sltsolem1  25540  nodenselem4  25556  nodenselem5  25557  nodenselem7  25559  nobndup  25572  nobnddown  25573  nofulllem5  25578  dfrdg4  25707  brbtwn2  25752  colinearalg  25757  axlowdimlem6  25794  axlowdimlem13  25801  axlowdimlem14  25802  axlowdim1  25806  axcontlem12  25822  btwnconn1lem13  25941  lineunray  25989  rankeq1o  26020  ordtoplem  26093  itg2addnclem3  26161  itgaddnclem2  26167  elicc3  26214  nn0prpw  26220  fdc  26343  prtlem90  26600  raldifsni  26628  cmpfiiin  26645  0dioph  26731  fphpd  26771  jm2.23  26961  wepwsolem  27010  uvcvv0  27111  sdrgacs  27381  isdomn3  27395  pm13.196a  27486  refsum2cnlem1  27579  fmul01lt1lem1  27585  stoweidlem14  27634  stoweidlem28  27648  stoweidlem55  27675  stoweid  27683  raaan2  27824  2reu4a  27838  afvfv0bi  27887  eqneqall  27943  pr1eqbg  27948  2f1fvneq  27962  dff14a  27963  euhash1  28002  swrdccatin1  28020  swrdccatin12b  28031  swrdccatin12c  28032  frgra3vlem1  28108  frgra3vlem2  28109  3vfriswmgralem  28112  2pthfrgra  28119  4cycl2vnunb  28125  n4cyclfrgra  28126  frgrancvvdeqlemA  28144  frgrancvvdeqlemB  28145  frgrancvvdeqlemC  28146  frgrawopreglem3  28153  frgrawopreglem4  28154  frgraregorufr0  28159  frgraregorufr  28160  usg2spot2nb  28172  sgnn  28242  onfrALTlem5  28343  onfrALTlem3  28345  en3lpVD  28670  onfrALTlem5VD  28710  onfrALTlem3VD  28712  a9e2ndeqVD  28734  a9e2ndeqALT  28757  bnj1109  28867  bnj1542  28938  bnj1253  29096  cvrval2  29761  cvrnbtwn2  29762  cvrnbtwn3  29763  cvlsupr3  29831  hlrelat5N  29887  cvrat4  29929  2at0mat0  30011  dalawlem13  30369  isltrn2N  30606  trlator0  30657  cdleme22b  30827  dochkrshp  31873  dochkrshp4  31876  lcfl6  31987  lclkrlem2x  32017
  Copyright terms: Public domain W3C validator