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 2791
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 2790 . 2 wff 𝐴𝐵
41, 2wceq 1480 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 196 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neii  2792  neir  2793  nne  2794  neneqd  2795  neqned  2797  eqneqall  2801  necon2bd  2806  necon1bd  2808  necon3d  2811  necon2d  2813  necon1bi  2818  necon1i  2823  necon3abid  2826  necon1bbid  2829  necon3bid  2834  necon3abii  2836  necon3bii  2842  neor  2881  neanior  2882  neorian  2884  nfne  2890  nfned  2891  nabbi  2892  dfpss2  3676  n0f  3909  ifnefalse  4076  snnzb  4231  raldifsni  4300  eqsn  4336  eqsnOLD  4337  n0snor2el  4339  opthpr  4359  unissint  4473  iununi  4583  disji2  4609  opthneg  4920  opab0  4977  xpcan  5539  xpcan2  5540  xpima  5545  unixpid  5639  unizlim  5813  2f1fvneq  6482  dff14a  6492  orduniorsuc  6992  dflim3  7009  tfindsg  7022  nn0suc  7052  findsg  7055  suppvalbr  7259  wfrlem16  7390  tz7.49  7500  oevn0  7555  php  8104  1sdom  8123  fimaxg  8167  fiint  8197  wemapsolem  8415  card2on  8419  brwdomn0  8434  domwdom  8439  rankxplim2  8703  rankxplim3  8704  carden2a  8752  dfackm  8948  fin23lem14  9115  fin1a2lem12  9193  axcc2lem  9218  ac6num  9261  zorn2lem4  9281  zorn2lem7  9284  brdom3  9310  iundom2g  9322  r1tskina  9564  1re  9999  ltlen  10098  uzm1  11678  xrnemnf  11911  xrnepnf  11912  ioo0  12158  ico0  12179  ioc0  12180  icc0  12181  elfznelfzo  12530  elfznelfzob  12531  injresinjlem  12544  fleqceilz  12609  fsuppmapnn0fiubex  12748  sq01  12942  hash1snb  13163  hashgt12el  13166  hashgt12el2  13167  hashfun  13180  hash2prde  13206  hashge2el2dif  13216  fundmge2nop0  13229  swrdccatin1  13436  repswcshw  13511  cshw1  13521  xptrrel  13669  incexc2  14514  sqrt2irr  14922  divalglem8  15066  ndvdssub  15076  algcvgblem  15233  lcmcllem  15252  lcmfunsnlem2lem2  15295  lcmfunsnlem2  15296  ncoprmgcdne1b  15306  isprm2lem  15337  isprm3  15339  isprm4  15340  ramcl2lem  15656  cshwshashlem1  15745  cshwshash  15754  sgrp2nmndlem3  17352  sgrp2rid2  17353  sgrp2nmndlem5  17356  symg2bas  17758  symgextf  17777  symgextfv  17778  odlem1  17894  gexlem1  17934  dprdfeq0  18361  isnirred  18640  isirred2  18641  drngmul0or  18708  drngmuleq0  18710  lvecvs0or  19048  lvecvscan  19051  isnzr2  19203  isdomn2  19239  cply1mul  19604  gsummoncoe1  19614  domnchr  19820  psgndiflemB  19886  dmatmul  20243  mulmarep1gsum1  20319  mulmarep1gsum2  20320  mdetdiag  20345  mdetunilem8  20365  mdetunilem9  20366  madurid  20390  mp2pm2mplem4  20554  fvmptnn04if  20594  fvmptnn04ifb  20596  elcls  20817  opnnei  20864  ist0-3  21089  ist1-2  21091  dfconn2  21162  cnconn  21165  pthaus  21381  xkohaus  21396  hausflim  21725  cldsubg  21854  bcth  23066  ioorinv  23284  tdeglem4  23758  fta1b  23867  plydivex  23990  plyexmo  24006  aalioulem3  24027  dvradcnv  24113  logtayllem  24339  logtayl  24340  cxpcl  24354  recxpcl  24355  logrec  24435  isosctrlem2  24483  efrlim  24630  muval2  24794  musum  24851  dchrelbas2  24896  dchrelbas4  24902  dchrfi  24914  dchrptlem3  24925  dchrsum2  24927  sumdchr2  24929  lgscllem  24963  2sqb  25091  dchrvmasumiflem2  25125  rpvmasum2  25135  padicabv  25253  padicabvf  25254  padicabvcxp  25255  tglowdim1i  25330  tgbtwnconn1  25404  colline  25478  colmid  25517  lmimid  25620  lmiisolem  25622  brbtwn2  25719  colinearalg  25724  axlowdimlem6  25761  axlowdimlem14  25769  axcontlem12  25789  incistruhgr  25904  umgr2edg1  26030  nb3grprlem1  26203  1egrvtxdg0  26327  wlkdlem4  26485  lfgriswlk  26488  pthdlem2  26567  wwlksnext  26691  clwlkclwwlklem2a4  26799  clwwisshclwwsn  26829  1wlkdlem4  26900  eupth2lem1  26978  eupth2lem3lem4  26991  frgr3vlem1  27035  frgr3vlem2  27036  3vfriswmgrlem  27039  4cycl2vnunb  27052  frgrncvvdeqlemB  27069  frgrregorufr  27082  frgrreg  27140  frgrregord013  27141  nvmul0or  27393  nmogtmnf  27513  hvmul0or  27770  hvmulcan  27817  hvmulcan2  27818  hiidge0  27843  bcsiALT  27924  shne0i  28195  nonbooli  28398  nmopgtmnf  28615  unopbd  28762  nmcfnlbi  28799  nmopcoi  28842  chirredi  29141  mdsymlem5  29154  sumdmdlem2  29166  disji2f  29276  imadifxp  29300  aciunf1  29346  2sqcoprm  29474  sitgaddlemb  30233  sgn3da  30426  plymulx  30447  bnj1109  30618  bnj1542  30688  bnj1253  30846  subfacp1lem6  30928  cvmsdisj  31013  sltval2  31563  sltres  31571  noseponlem  31575  nosepon  31576  nodenselem4  31600  nodenselem5  31601  nodenselem7  31603  nobndup  31616  nobnddown  31617  btwnconn1lem13  31901  lineunray  31949  rankeq1o  31973  elicc3  32006  nn0prpw  32013  ordtoplem  32129  icorempt2  32870  matunitlindflem1  33076  poimirlem1  33081  poimirlem14  33094  poimirlem16  33096  poimirlem19  33099  poimirlem23  33103  poimirlem25  33105  poimirlem26  33106  itg2addnclem3  33134  itgaddnclem2  33140  fdc  33212  ismgmOLD  33320  cvrval2  34080  cvrnbtwn2  34081  cvrnbtwn3  34082  cvlsupr3  34150  cvrat4  34248  2at0mat0  34330  dalawlem13  34688  isltrn2N  34925  trlator0  34977  cdleme22b  35148  dochkrshp  36194  dochkrshp4  36197  lcfl6  36308  lclkrlem2x  36338  fphpd  36899  jm2.23  37082  sdrgacs  37291  isdomn3  37302  iunrelexp0  37514  ntrneineine1lem  37903  pm13.196a  38136  onfrALTlem5  38278  onfrALTlem3  38280  en3lpVD  38602  onfrALTlem5VD  38643  onfrALTlem3VD  38645  ax6e2ndeqVD  38667  ax6e2ndeqALT  38689  isosctrlem1ALT  38692  ndisj2  38740  limsupre2lem  39392  cncfiooicclem1  39441  iblcncfioo  39531  stoweidlem28  39582  sge0iunmpt  39972  raaan2  40509  afvfv0bi  40566  2ffzoeq  40665  iccpartiltu  40686  iccpartlt  40688  icceuelpartlem  40699  cshword2  40766  lighneallem4  40856  oddprmALTV  40927  evenprm2  40952  upgrwlkupwlk  41039  copisnmnd  41127  fdmdifeqresdif  41438  pgrpgt2nabl  41465  islindeps  41560  lincext1  41561  lindslinindsimp2lem5  41569  snlindsntor  41578  ldepslinc  41616  m1modmmod  41634
  Copyright terms: Public domain W3C validator