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

Definition df-ne 2450
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 2448 . 2  wff  A  =/= 
B
41, 2wceq 1624 . . 3  wff  A  =  B
54wn 5 . 2  wff  -.  A  =  B
63, 5wb 178 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  nne  2452  exmidne  2454  nonconne  2455  neeq1  2456  neeq2  2457  neneqd  2464  necon3abii  2478  necon3bii  2480  necon3abid  2481  necon3bid  2483  necon3d  2486  necon1ai  2490  necon1i  2492  necon2bd  2497  necon2d  2498  necon1abii  2499  necon1bbii  2500  necon1abid  2501  necon1bbid  2502  necon2abid  2505  necon2bbid  2506  necon4abid  2512  necon1ad  2515  neor  2532  neanior  2533  neorian  2535  nemtbir  2536  nfne  2541  nfned  2543  dfpss2  3263  ne0i  3463  neq0  3467  ifnefalse  3575  eqsn  3777  snsssn  3783  opthpr  3792  unissint  3888  iununi  3988  disji2  4012  ord0eln0  4446  nsuceq0  4472  unizlim  4509  orduniorsuc  4621  dflim3  4638  tfindsg  4651  nn0suc  4680  findsg  4683  frsn  4760  xpcan  5112  xpcan2  5113  unixpid  5206  fv2  5482  fvprc  5483  tz7.49  6453  oevn0  6510  2dom  6929  sdomdif  7005  2pwne  7013  map2xp  7027  mapdom2  7028  php  7041  1sdom  7061  fimaxg  7100  fiint  7129  wemapso2lem  7261  card2on  7264  brwdomn0  7279  domwdom  7284  rankxplim2  7546  rankxplim3  7547  carden2a  7595  pm54.43lem  7628  dfackm  7788  fin23lem14  7955  fin1a2lem12  8033  axcc2lem  8058  ac6num  8102  ac9  8106  ac9s  8116  zorn2lem4  8122  zorn2lem7  8125  brdom3  8149  iundom2g  8158  canthp1lem2  8271  r1tskina  8400  ax1ne0  8778  1re  8833  ltlen  8918  ine0  9211  recgt0ii  9658  inelr  9732  nnunb  9957  uzm1  10254  xrnemnf  10456  xrnepnf  10457  xrltnr  10458  pnfnlt  10463  nltmnf  10464  xrltlen  10476  ioo0  10676  ico0  10697  ioc0  10698  icc0  10699  fzm1  10857  sq01  11218  hashfun  11384  incexc2  12292  sqr2irr  12522  divalglem8  12594  ndvdssub  12601  algcvgblem  12742  isprm2lem  12760  isprm2  12761  isprm3  12762  isprm4  12763  isprm5  12786  ramcl2lem  13051  xpsfrnel2  13462  setcepi  13915  odlem1  14845  gexlem1  14885  dprdfeq0  15252  isnirred  15477  isirred2  15478  drngmul0or  15528  drngmuleq0  15530  lvecvs0or  15856  lvecvscan  15859  lspsncv0  15894  isnzr2  16010  isdomn2  16035  domnchr  16481  elcls  16805  opnnei  16852  ist0-3  17068  ist1-2  17070  dfcon2  17140  cnconn  17143  pthaus  17327  xkohaus  17342  trfbas  17534  fbunfip  17559  trfil2  17577  hausflim  17671  alexsub  17734  cldsubg  17788  bcth  18746  iundisj2  18901  ioorf  18923  ioorinv  18926  tdeglem4  19441  fta1b  19550  plydivex  19672  vieta1lem2  19686  plyexmo  19688  aalioulem3  19709  dvtaylp  19744  dvradcnv  19792  sinhalfpilem  19829  coseq1  19885  logtayllem  20001  logtayl  20002  cxpcl  20016  recxpcl  20017  logrec  20112  isosctrlem2  20114  efrlim  20259  muval2  20367  musum  20426  dchrelbas2  20471  dchrelbas4  20477  dchrfi  20489  dchrptlem3  20500  dchrsum2  20502  sumdchr2  20504  lgsfcl2  20536  lgscllem  20537  lgsval2lem  20540  2sqb  20612  dchrvmasumiflem2  20646  rpvmasum2  20656  dchrisumn0  20665  padicabv  20774  padicabvf  20775  padicabvcxp  20776  ismgm  20980  vcoprne  21128  nvmul0or  21203  nmogtmnf  21341  hvmul0or  21597  hvmulcan  21644  hvmulcan2  21645  hiidge0  21670  bcsiALT  21751  norm1exi  21822  shne0i  22020  nonbooli  22223  nmopgtmnf  22441  unopbd  22588  nmcfnlbi  22625  nmopcoi  22668  strlem1  22823  largei  22840  chirredi  22967  mdsymlem5  22980  sumdmdlem2  22992  ballotlemi1  23055  ballotlemii  23056  ballotlemfrcn0  23082  subfacp1lem6  23121  pconcon  23167  cvmsdisj  23206  cvmscld  23209  eupath2lem1  23306  eupath  23310  pm2.61iine  23485  dfrdg2  23554  wfrlem16  23673  sltval2  23711  nosgnn0  23713  nosgnn0i  23714  sltintdifex  23718  sltres  23719  axsltsolem1  23723  axdenselem3  23739  axdenselem4  23740  axdenselem5  23741  axdenselem7  23743  axfelem9  23756  axfelem10  23757  axfelem15  23762  axfelem18  23765  axfelem22  23769  dfrdg4  23896  brbtwn2  23941  colinearalg  23946  axlowdimlem6  23983  axlowdimlem13  23990  axlowdimlem14  23991  axlowdim1  23995  axcontlem12  24011  btwnconn1lem13  24130  lineunray  24178  rankeq1o  24209  ordtoplem  24282  vxveqv  24453  repcpwti  24561  dmse1  25003  iintlem1  25010  hdrmp  25106  lineval5a  25488  lineval6a  25489  lppotoslem  25543  lppotos  25544  xsyysx  25545  bsstrs  25546  nbssntrs  25547  pdiveql  25568  hpd  25569  elicc3  25628  nn0prpw  25639  fdc  25855  maxidln0  26070  prtlem90  26123  raldifsni  26153  cmpfiiin  26172  0dioph  26258  fphpd  26299  pellexlem6  26319  jm2.23  26489  wepwsolem  26538  uvcvv0  26639  sdrgacs  26909  isdomn3  26923  pm13.196a  27014  compneOLD  27043  fnchoice  27100  refsum2cnlem1  27108  fmul01lt1lem1  27114  stoweidlem14  27163  stoweidlem23  27172  stoweidlem28  27177  stoweidlem35  27184  stoweidlem39  27188  stoweidlem55  27204  stoweidlem58  27207  stoweid  27212  raaan2  27333  2reu4a  27347  afvfv0bi  27395  sgnn  27512  onfrALTlem5  27579  onfrALTlem3  27581  en3lpVD  27890  onfrALTlem5VD  27930  onfrALTlem3VD  27932  a9e2ndeqVD  27954  a9e2ndeqALT  27977  bnj1109  28086  bnj1542  28157  bnj1253  28315  cvrval2  28732  cvrnbtwn2  28733  cvrnbtwn3  28734  cvlsupr3  28802  hlrelat5N  28858  cvrat4  28900  2at0mat0  28982  dalawlem13  29340  isltrn2N  29577  trlator0  29628  cdleme22b  29798  dochkrshp  30844  dochkrshp4  30847  lcfl6  30958  lclkrlem2x  30988  hdmapip0  31376
  Copyright terms: Public domain W3C validator