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

Theorem neeq1 2982
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
Assertion
Ref Expression
neeq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem neeq1
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21neeq1d 2979 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1620  wne 2920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842  df-cleq 2741  df-ne 2921
This theorem is referenced by:  nelrdva  3546  psseq1  3824  ssdifsnOLD  4452  n0snor2el  4497  0inp0  4974  nnullss  5067  opeqex  5098  fri  5216  frsn  5334  xp11  5715  limeq  5884  tz6.12i  6363  fveqressseq  6506  funopsn  6564  fprg  6573  tpres  6618  f1dom3el3dif  6677  f1prex  6690  isofrlem  6741  f1oweALT  7305  frxp  7443  suppimacnv  7462  elqsn0  7971  frfi  8358  fiint  8390  marypha1lem  8492  dfac8alem  9013  dfac8clem  9016  aceq3lem  9104  dfac5lem3  9109  dfac5lem4  9110  dfac5  9112  dfac2b  9114  dfac2OLD  9116  dfac9  9121  kmlem1  9135  kmlem12  9146  kmlem14  9148  fin2i  9280  isfin2-2  9304  fin23lem21  9324  fin1a2lem10  9394  axcc2lem  9421  dominf  9430  ac5b  9463  zornn0g  9490  axdclem  9504  dominfac  9558  elwina  9671  elina  9672  iswun  9689  rankcf  9762  axrrecex  10147  elimne0  10193  1re  10202  recex  10822  xnn0nemnf  11537  uzn0  11866  qreccl  11972  xrnemnf  12115  xrnepnf  12116  xnn0n0n1ge2b  12129  fztpval  12566  expcl2lem  13037  hashnemnf  13297  hashneq0  13318  hashge2el2difr  13426  hashdmpropge2  13428  relexp1g  13936  ntrivcvgn0  14800  ntrivcvgmullem  14803  fprodntriv  14842  divalglem7  15295  divalg  15299  gcdcllem1  15394  gcdcllem3  15396  pcpre1  15720  pcqmul  15731  pcqcl  15734  prmgaplem3  15930  prmgaplem4  15931  xpscfv  16395  xpsfrnel  16396  mreintcl  16428  isdrs  17106  isipodrs  17333  sgrp2rid2ex  17586  frgpuptinv  18355  isdrngrd  18946  isnzr2  19436  psgnodpmr  20109  lindfrn  20333  dmatelnd  20475  dmatmul  20476  mdetdiaglem  20577  mdetunilem1  20591  fvmptnn04ifa  20828  chfacfscmulgsum  20838  chfacfpmmulgsum  20842  fiinopn  20879  hausnei  21305  dfconn2  21395  2ndcdisj  21432  regr1lem2  21716  isfbas  21805  ioorinv  23515  ioorcl  23516  vitalilem2  23548  vitalilem3  23549  vitali  23552  itg1climres  23651  mbfi1fseqlem4  23655  dvferm1lem  23917  dvferm2lem  23919  isuc1p  24070  ismon1p  24072  ply1remlem  24092  plydivlem4  24221  aannenlem1  24253  aannenlem2  24254  lgsne0  25230  lgsqr  25246  axtg5seg  25534  axtgupdim2  25540  axtgeucl  25541  axlowdim1  26009  structgrssvtxlemOLD  26085  lpvtx  26133  umgrnloopv  26171  usgrnloopvALT  26263  umgrvad2edg  26275  cusgrfilem2  26533  pthdlem2lem  26844  iswwlks  26910  iswwlksnx  26914  2pthdlem1  27021  isclwwlk  27078  3pthdlem1  27287  upgr3v3e3cycl  27303  upgr4cycl4dv4e  27308  eupth2lem2  27342  eupth2lem3lem4  27354  eupth2lem3lem6  27356  3cyclfrgrrn1  27410  4cycl2vnunb  27415  frgrreg  27533  norm1exi  28387  shintcl  28469  chintcl  28471  chne0  28633  elspansn2  28706  eigre  28974  eigorth  28977  kbpj  29095  superpos  29493  hatomic  29499  xrge0iifhom  30263  xrge0iif1  30264  esumpr2  30409  sibfof  30682  signswn0  30917  signswch  30918  signstfvneq0  30929  axtgupdim2OLD  31026  bnj168  31076  bnj970  31295  bnj1154  31345  subfacp1lem1  31439  erdszelem8  31458  indispconn  31494  cvmsss2  31534  nepss  31877  frmin  32019  elwlim  32045  nolesgn2ores  32102  nosepdmlem  32110  nosupbnd1lem3  32133  nosupbnd1lem5  32135  nosupbnd2lem1  32138  dfrdg4  32335  fvray  32525  linedegen  32527  fvline  32528  hilbert1.1  32538  rankeq1o  32555  unblimceq0lem  32774  knoppndvlem21  32800  poimirlem1  33692  poimirlem17  33708  poimirlem20  33711  poimirlem32  33723  itg2addnclem3  33745  neificl  33831  isdrngo3  34040  ispridl  34115  ismaxidl  34121  islshp  34738  lsatn0  34758  lshpset2N  34878  atlex  35075  hlsuprexch  35139  3dimlem1  35216  llni2  35270  lplni2  35295  2llnjN  35325  lvoli2  35339  2lplnj  35378  islinei  35498  lnatexN  35537  llnexchb2  35627  lhpmatb  35789  cdleme40m  36226  cdlemftr3  36324  cdlemk28-3  36667  cdlemk35s  36696  cdlemk39s  36698  cdlemk42  36700  dnnumch1  38085  aomclem3  38097  aomclem8  38102  dfac11  38103  dfacbasgrp  38149  ax6e2ndeq  39246  ax6e2ndeqVD  39613  fnchoice  39656  fiiuncl  39702  disjrnmpt2  39843  idlimc  40330  limcperiod  40332  limclner  40355  cnrefiisp  40528  climxlim2lem  40543  fperdvper  40605  stoweidlem35  40724  stoweidlem43  40732  stoweidlem59  40748  fourierdlem76  40871  etransclem47  40970  nnfoctbdjlem  41144  elprneb  41774  nrhmzr  42352
  Copyright terms: Public domain W3C validator