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

Definition df-ne 2448
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 2446 . 2  wff  A  =/= 
B
41, 2wceq 1623 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 176 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  nne  2450  exmidne  2452  nonconne  2453  neeq1  2454  neeq2  2455  neneqd  2462  necon3abii  2476  necon3bii  2478  necon3abid  2479  necon3bid  2481  necon3d  2484  necon1ai  2488  necon1i  2490  necon2bd  2495  necon2d  2496  necon1abii  2497  necon1bbii  2498  necon1abid  2499  necon1bbid  2500  necon2abid  2503  necon2bbid  2504  necon4abid  2510  necon1ad  2513  neor  2530  neanior  2531  neorian  2533  nemtbir  2534  nfne  2539  nfned  2541  dfpss2  3261  ne0i  3461  neq0  3465  ifnefalse  3573  eqsn  3775  snsssn  3781  opthpr  3790  unissint  3886  iununi  3986  disji2  4010  ord0eln0  4446  nsuceq0  4472  unizlim  4509  orduniorsuc  4621  dflim3  4638  tfindsg  4651  nn0suc  4680  findsg  4683  frsn  4760  xpcan  5112  xpcan2  5113  unixpid  5207  tz7.49  6457  oevn0  6514  2dom  6933  sdomdif  7009  2pwne  7017  map2xp  7031  mapdom2  7032  php  7045  1sdom  7065  fimaxg  7104  fiint  7133  wemapso2lem  7265  card2on  7268  brwdomn0  7283  domwdom  7288  rankxplim2  7550  rankxplim3  7551  carden2a  7599  pm54.43lem  7632  dfackm  7792  fin23lem14  7959  fin1a2lem12  8037  axcc2lem  8062  ac6num  8106  ac9  8110  ac9s  8120  zorn2lem4  8126  zorn2lem7  8129  brdom3  8153  iundom2g  8162  canthp1lem2  8275  r1tskina  8404  ax1ne0  8782  1re  8837  ltlen  8922  ine0  9215  recgt0ii  9662  inelr  9736  nnunb  9961  uzm1  10258  xrnemnf  10460  xrnepnf  10461  xrltnr  10462  pnfnlt  10467  nltmnf  10468  xrltlen  10480  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  fzm1  10862  sq01  11223  hashfun  11389  incexc2  12297  sqr2irr  12527  divalglem8  12599  ndvdssub  12606  algcvgblem  12747  isprm2lem  12765  isprm2  12766  isprm3  12767  isprm4  12768  isprm5  12791  ramcl2lem  13056  xpsfrnel2  13467  setcepi  13920  odlem1  14850  gexlem1  14890  dprdfeq0  15257  isnirred  15482  isirred2  15483  drngmul0or  15533  drngmuleq0  15535  lvecvs0or  15861  lvecvscan  15864  lspsncv0  15899  isnzr2  16015  isdomn2  16040  domnchr  16486  elcls  16810  opnnei  16857  ist0-3  17073  ist1-2  17075  dfcon2  17145  cnconn  17148  pthaus  17332  xkohaus  17347  trfbas  17539  fbunfip  17564  trfil2  17582  hausflim  17676  alexsub  17739  cldsubg  17793  bcth  18751  iundisj2  18906  ioorf  18928  ioorinv  18931  tdeglem4  19446  fta1b  19555  plydivex  19677  vieta1lem2  19691  plyexmo  19693  aalioulem3  19714  dvtaylp  19749  dvradcnv  19797  sinhalfpilem  19834  coseq1  19890  logtayllem  20006  logtayl  20007  cxpcl  20021  recxpcl  20022  logrec  20117  isosctrlem2  20119  efrlim  20264  muval2  20372  musum  20431  dchrelbas2  20476  dchrelbas4  20482  dchrfi  20494  dchrptlem3  20505  dchrsum2  20507  sumdchr2  20509  lgsfcl2  20541  lgscllem  20542  lgsval2lem  20545  2sqb  20617  dchrvmasumiflem2  20651  rpvmasum2  20661  dchrisumn0  20670  padicabv  20779  padicabvf  20780  padicabvcxp  20781  ismgm  20987  vcoprne  21135  nvmul0or  21210  nmogtmnf  21348  hvmul0or  21604  hvmulcan  21651  hvmulcan2  21652  hiidge0  21677  bcsiALT  21758  norm1exi  21829  shne0i  22027  nonbooli  22230  nmopgtmnf  22448  unopbd  22595  nmcfnlbi  22632  nmopcoi  22675  strlem1  22830  largei  22847  chirredi  22974  mdsymlem5  22987  sumdmdlem2  22999  ballotlemi1  23061  ballotlemii  23062  ballotlemfrcn0  23088  xpima  23202  disji2f  23354  disjif2  23358  iundisj2fi  23364  iundisj2f  23366  itgmcntTMP  23588  ind1a  23604  subfacp1lem6  23716  pconcon  23762  cvmsdisj  23801  cvmscld  23804  eupath2lem1  23901  eupath  23905  pm2.61iine  24081  dfrdg2  24152  wfrlem16  24271  sltval2  24310  nosgnn0  24312  nosgnn0i  24313  sltintdifex  24317  sltres  24318  sltsolem1  24322  nodenselem3  24337  nodenselem4  24338  nodenselem5  24339  nodenselem7  24341  nobndup  24354  nobnddown  24355  nofulllem5  24360  dfrdg4  24488  brbtwn2  24533  colinearalg  24538  axlowdimlem6  24575  axlowdimlem13  24582  axlowdimlem14  24583  axlowdim1  24587  axcontlem12  24603  btwnconn1lem13  24722  lineunray  24770  rankeq1o  24801  ordtoplem  24874  vxveqv  25054  repcpwti  25161  dmse1  25603  iintlem1  25610  hdrmp  25706  lineval5a  26088  lineval6a  26089  lppotoslem  26143  lppotos  26144  xsyysx  26145  bsstrs  26146  nbssntrs  26147  pdiveql  26168  hpd  26169  elicc3  26228  nn0prpw  26239  fdc  26455  maxidln0  26670  prtlem90  26723  raldifsni  26753  cmpfiiin  26772  0dioph  26858  fphpd  26899  pellexlem6  26919  jm2.23  27089  wepwsolem  27138  uvcvv0  27239  sdrgacs  27509  isdomn3  27523  pm13.196a  27614  compneOLD  27643  fnchoice  27700  refsum2cnlem1  27708  fmul01lt1lem1  27714  stoweidlem14  27763  stoweidlem23  27772  stoweidlem28  27777  stoweidlem35  27784  stoweidlem39  27788  stoweidlem55  27804  stoweidlem58  27807  stoweid  27812  raaan2  27953  2reu4a  27967  afvfv0bi  28015  usgraedgprv  28122  nbusgra  28143  nbgranself  28149  uvtx01vtx  28164  frgra3vlem1  28178  frgra3vlem2  28179  3vfriswmgralem  28182  sgnn  28251  onfrALTlem5  28307  onfrALTlem3  28309  en3lpVD  28621  onfrALTlem5VD  28661  onfrALTlem3VD  28663  a9e2ndeqVD  28685  a9e2ndeqALT  28708  bnj1109  28818  bnj1542  28889  bnj1253  29047  cvrval2  29464  cvrnbtwn2  29465  cvrnbtwn3  29466  cvlsupr3  29534  hlrelat5N  29590  cvrat4  29632  2at0mat0  29714  dalawlem13  30072  isltrn2N  30309  trlator0  30360  cdleme22b  30530  dochkrshp  31576  dochkrshp4  31579  lcfl6  31690  lclkrlem2x  31720  hdmapip0  32108
  Copyright terms: Public domain W3C validator