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

Definition df-ne 3015
Description: Define inequality. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
df-ne (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)

Detailed syntax breakdown of Definition df-ne
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wne 3014 . 2 wff 𝐴𝐵
41, 2wceq 1538 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 209 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neii  3016  neir  3017  nne  3018  neneqd  3019  neqned  3021  eqneqall  3025  necon2bd  3030  necon1bd  3032  necon3d  3035  necon2d  3037  necon1bi  3042  necon1i  3047  necon3abid  3050  necon1bbid  3053  necon3bid  3058  necon3abii  3060  necon3bii  3066  neor  3105  neanior  3106  neorian  3108  nfne  3114  nfned  3115  nabbi  3116  nelb  3260  dfpss2  4048  dfdif3  4077  n0f  4290  2nreu  4376  raaan2  4447  ifnefalse  4462  snnzb  4639  raldifsni  4712  eqsn  4746  n0snor2el  4748  opthpr  4766  opthprneg  4779  unissint  4886  iununi  5007  disji2  5035  opthneg  5361  opab0  5429  xpcan  6022  xpcan2  6023  xpima  6028  unixpid  6124  unizlim  6296  dff14a  7022  orduniorsuc  7541  dflim3  7558  tfindsg  7571  nn0suc  7602  findsg  7606  suppvalbr  7832  wfrlem16  7968  tz7.49  8079  oevn0  8138  php  8700  1sdom  8720  fimaxg  8764  fiint  8794  wemapsolem  9013  card2on  9017  brwdomn0  9032  rankxplim2  9308  rankxplim3  9309  updjudhf  9359  carden2a  9394  dfackm  9592  fin1a2lem12  9833  ac6num  9901  zorn2lem4  9921  zorn2lem7  9924  brdom3  9950  iundom2g  9962  r1tskina  10204  1re  10641  ltlen  10741  uzm1  12275  xrnemnf  12511  xrnepnf  12512  ioo0  12762  ico0  12783  ioc0  12784  icc0  12785  elfznelfzo  13148  elfznelfzob  13149  injresinjlem  13163  fleqceilz  13228  fsuppmapnn0fiubex  13366  sq01  13593  hash1snb  13787  hashgt12el  13790  hashgt12el2  13791  hashfun  13805  hash2prde  13835  hashge2el2dif  13845  fundmge2nop0  13857  repswcshw  14176  cshw1  14186  incexc2  15195  sqrt2irr  15604  divalglem8  15751  ndvdssub  15760  algcvgblem  15921  lcmcllem  15940  lcmfunsnlem2  15984  isprm3  16027  isprm4  16028  2mulprm  16037  ramcl2lem  16345  cshwshashlem1  16431  cshwshash  16440  smndex2dnrinv  18082  sgrp2nmndlem3  18092  sgrp2nmndlem5  18096  symg2bas  18523  odfval  18662  dprdfeq0  19146  isnirred  19455  isirred2  19456  drngmul0or  19525  drngmuleq0  19527  sdrgacs  19582  lvecvs0or  19882  lvecvscan  19885  isnzr2  20038  isdomn2  20074  domnchr  20233  gsummoncoe1  20942  dmatmul  21111  mulmarep1gsum2  21188  mdetunilem8  21233  mp2pm2mplem4  21423  fvmptnn04if  21463  elcls  21687  opnnei  21734  ist0-3  21959  ist1-2  21961  dfconn2  22033  cnconn  22036  pthaus  22252  xkohaus  22267  hausflim  22595  cldsubg  22725  bcth  23942  ioorinv  24189  tdeglem4  24670  fta1b  24779  plydivex  24902  aalioulem3  24939  dvradcnv  25025  cxpcl  25274  recxpcl  25275  logrec  25358  isosctrlem2  25414  efrlim  25564  muval2  25728  musum  25785  dchrelbas2  25830  dchrelbas4  25836  dchrfi  25848  dchrptlem3  25859  dchrsum2  25861  sumdchr2  25863  lgscllem  25897  2sqb  26025  2sqcoprm  26028  dchrvmasumiflem2  26095  rpvmasum2  26105  padicabv  26223  padicabvf  26224  padicabvcxp  26225  tglowdim1i  26304  tgbtwnconn1  26378  colline  26452  colmid  26491  lmimid  26597  lmiisolem  26599  brbtwn2  26708  colinearalg  26713  axlowdimlem6  26750  axlowdimlem14  26758  axcontlem12  26778  incistruhgr  26881  umgr2edg1  27010  nb3grprlem1  27179  1egrvtxdg0  27310  vtxdginducedm1lem4  27341  wlkdlem4  27484  lfgriswlk  27487  pthdlem2  27566  wwlksnext  27688  clwwlknclwwlkdif  27773  clwlkclwwlklem2a4  27791  clwwisshclwwsn  27810  1wlkdlem4  27934  eupth2lem1  28012  eupth2lem3lem4  28025  frgr3vlem1  28067  frgr3vlem2  28068  3vfriswmgrlem  28071  4cycl2vnunb  28084  frgrncvvdeqlem8  28100  frgrregorufr  28119  frgrreg  28188  frgrregord013  28189  9p10ne21fool  28265  nvmul0or  28442  nmogtmnf  28562  hvmul0or  28817  hvmulcan  28864  hvmulcan2  28865  hiidge0  28890  bcsiALT  28971  shne0i  29240  nonbooli  29443  nmopgtmnf  29660  unopbd  29807  nmcfnlbi  29844  nmopcoi  29887  chirredi  30186  mdsymlem5  30199  sumdmdlem2  30211  nelbOLD  30248  disji2f  30346  aciunf1  30427  fzne1  30532  hashxpe  30550  sitgaddlemb  31691  sgn3da  31884  plymulx  31903  bnj1109  32143  bnj1542  32214  bnj1253  32374  dff15  32438  lfuhgr3  32451  dfacycgr1  32476  subfacp1lem6  32517  cvmsdisj  32602  satffunlem1lem1  32734  satffunlem2lem1  32736  satffun  32741  frrlem14  33221  sltval2  33248  sltres  33254  noseponlem  33256  nosepon  33257  nosepeq  33274  nosupbnd2lem1  33300  noetalem3  33304  btwnconn1lem13  33645  lineunray  33693  rankeq1o  33717  elicc3  33750  nn0prpw  33756  ordtoplem  33868  bj-snmoore  34500  irrdifflemf  34711  icorempo  34740  matunitlindflem1  35025  poimirlem1  35030  poimirlem14  35043  poimirlem16  35045  poimirlem19  35048  poimirlem23  35052  poimirlem25  35054  poimirlem26  35055  itg2addnclem3  35082  itgaddnclem2  35088  fdc  35155  ismgmOLD  35260  cvrval2  36542  cvrnbtwn2  36543  cvrnbtwn3  36544  cvlsupr3  36612  cvrat4  36711  2at0mat0  36793  dalawlem13  37151  isltrn2N  37388  trlator0  37439  cdleme22b  37609  dochkrshp  38654  dochkrshp4  38657  lcfl6  38768  lclkrlem2x  38798  metakunt6  39328  metakunt7  39329  metakunt11  39333  metakunt22  39344  nnn1suc  39425  sn-00id  39497  remulid2  39527  fphpd  39701  jm2.23  39881  isdomn3  40092  dfsucon  40175  iunrelexp0  40347  ntrneineine1lem  40734  pm13.196a  41066  onfrALTlem5  41196  onfrALTlem3  41198  en3lpVD  41499  onfrALTlem5VD  41539  onfrALTlem3VD  41541  ax6e2ndeqVD  41563  ax6e2ndeqALT  41585  isosctrlem1ALT  41588  ndisj2  41633  limsupre2lem  42319  cncfiooicclem1  42488  iblcncfioo  42573  stoweidlem28  42623  sge0iunmpt  43010  afvfv0bi  43661  2ffzoeq  43838  iccpartiltu  43892  iccpartlt  43894  icceuelpartlem  43905  lighneallem4  44081  oddprmALTV  44158  evenprm2  44185  odd2prm2  44189  even3prm2  44190  upgrwlkupwlk  44321  copisnmnd  44382  pgrpgt2nabl  44721  islindeps  44815  lincext1  44816  lindslinindsimp2lem5  44824  snlindsntor  44833  ldepslinc  44871  m1modmmod  44888  rrx2linest  45109  line2ylem  45118  line2xlem  45120
  Copyright terms: Public domain W3C validator