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

Theorem neeq1 2853
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 2850 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wne 2791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-ne 2792
This theorem is referenced by:  nelrdva  3411  psseq1  3686  ssdifsn  4309  n0snor2el  4355  0inp0  4828  nnullss  4921  opeqex  4952  fri  5066  frsn  5179  xp11  5557  limeq  5723  tz6.12i  6201  fveqressseq  6341  funopsn  6398  fprg  6407  tpres  6451  f1dom3el3dif  6511  f1prex  6524  isofrlem  6575  f1oweALT  7137  frxp  7272  suppimacnv  7291  elqsn0  7801  frfi  8190  fiint  8222  marypha1lem  8324  dfac8alem  8837  dfac8clem  8840  aceq3lem  8928  dfac5lem3  8933  dfac5lem4  8934  dfac5  8936  dfac2  8938  dfac9  8943  kmlem1  8957  kmlem12  8968  kmlem14  8970  fin2i  9102  isfin2-2  9126  fin23lem21  9146  fin1a2lem10  9216  axcc2lem  9243  dominf  9252  ac5b  9285  zornn0g  9312  axdclem  9326  dominfac  9380  elwina  9493  elina  9494  iswun  9511  rankcf  9584  axrrecex  9969  elimne0  10015  1re  10024  recex  10644  xnn0nemnf  11359  uzn0  11688  qreccl  11793  xrnemnf  11936  xrnepnf  11937  xnn0n0n1ge2b  11950  fztpval  12387  expcl2lem  12855  hashnemnf  13115  hashneq0  13138  hashge2el2difr  13246  hashdmpropge2  13248  relexp1g  13747  ntrivcvgn0  14611  ntrivcvgmullem  14614  fprodntriv  14653  divalglem7  15103  divalg  15107  gcdcllem1  15202  gcdcllem3  15204  isprm2lem  15375  pcpre1  15528  pcqmul  15539  pcqcl  15542  prmgaplem3  15738  prmgaplem4  15739  xpscfv  16203  xpsfrnel  16204  mreintcl  16236  isdrs  16915  isipodrs  17142  sgrp2rid2ex  17395  frgpuptinv  18165  isdrngrd  18754  isnzr2  19244  psgnodpmr  19917  lindfrn  20141  dmatelnd  20283  dmatmul  20284  mdetdiaglem  20385  mdetunilem1  20399  fvmptnn04ifa  20636  chfacfscmulgsum  20646  chfacfpmmulgsum  20650  fiinopn  20687  hausnei  21113  dfconn2  21203  2ndcdisj  21240  regr1lem2  21524  isfbas  21614  ioorinv  23325  ioorcl  23326  vitalilem2  23359  vitalilem3  23360  vitali  23363  itg1climres  23462  mbfi1fseqlem4  23466  dvferm1lem  23728  dvferm2lem  23730  isuc1p  23881  ismon1p  23883  ply1remlem  23903  plydivlem4  24032  aannenlem1  24064  aannenlem2  24065  lgsne0  25041  lgsqr  25057  axtg5seg  25345  axtgupdim2  25351  axtgeucl  25352  axlowdim1  25820  structgrssvtxlemOLD  25896  lpvtx  25944  umgrnloopv  25982  usgrnloopvALT  26074  umgrvad2edg  26086  cusgrfilem2  26333  pthdlem2lem  26644  iswwlks  26709  iswwlksnx  26712  2pthdlem1  26807  isclwwlks  26861  3pthdlem1  27004  upgr3v3e3cycl  27020  upgr4cycl4dv4e  27025  eupth2lem2  27059  eupth2lem3lem4  27071  eupth2lem3lem6  27073  3cyclfrgrrn1  27129  4cycl2vnunb  27134  frgrreg  27222  norm1exi  28077  shintcl  28159  chintcl  28161  chne0  28323  elspansn2  28396  eigre  28664  eigorth  28667  kbpj  28785  superpos  29183  hatomic  29189  xrge0iifhom  29957  xrge0iif1  29958  esumpr2  30103  sibfof  30376  signswn0  30611  signswch  30612  signstfvneq0  30623  axtgupdim2OLD  30720  bnj168  30772  bnj970  30991  bnj1154  31041  subfacp1lem1  31135  erdszelem8  31154  indispconn  31190  cvmsss2  31230  nepss  31574  frmin  31713  elwlim  31743  elwlimOLD  31744  nolesgn2ores  31799  nosepdmlem  31807  nosupbnd1lem3  31830  nosupbnd1lem5  31832  nosupbnd2lem1  31835  dfrdg4  32033  fvray  32223  linedegen  32225  fvline  32226  hilbert1.1  32236  rankeq1o  32253  unblimceq0lem  32472  knoppndvlem21  32498  poimirlem1  33381  poimirlem17  33397  poimirlem20  33400  poimirlem32  33412  itg2addnclem3  33434  neificl  33520  isdrngo3  33729  ispridl  33804  ismaxidl  33810  islshp  34085  lsatn0  34105  lshpset2N  34225  atlex  34422  hlsuprexch  34486  3dimlem1  34563  llni2  34617  lplni2  34642  2llnjN  34672  lvoli2  34686  2lplnj  34725  islinei  34845  lnatexN  34884  llnexchb2  34974  lhpmatb  35136  cdleme40m  35574  cdlemftr3  35672  cdlemk28-3  36015  cdlemk35s  36044  cdlemk39s  36046  cdlemk42  36048  dnnumch1  37433  aomclem3  37445  aomclem8  37450  dfac11  37451  dfacbasgrp  37497  ax6e2ndeq  38595  ax6e2ndeqVD  38965  fnchoice  39008  fiiuncl  39054  disjrnmpt2  39191  idlimc  39658  limcperiod  39660  limclner  39683  fperdvper  39896  stoweidlem35  40015  stoweidlem43  40023  stoweidlem59  40039  fourierdlem76  40162  etransclem47  40261  nnfoctbdjlem  40435  elprneb  41059  nrhmzr  41638
  Copyright terms: Public domain W3C validator