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

Theorem neeq1 3078
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 3075 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  pm13.18  3097  nelrdva  3695  psseq1  4063  n0snor2el  4758  0inp0  5251  nnullss  5346  opeqex  5380  fri  5511  frsn  5633  xp11  6026  limeq  6197  tz6.12i  6690  fveqressseq  6840  funopsn  6903  fprg  6910  tpres  6956  f1dom3el3dif  7018  f1prex  7031  isofrlem  7082  f1oweALT  7664  frxp  7811  suppimacnv  7832  elqsn0  8356  frfi  8752  fiint  8784  marypha1lem  8886  eldju2ndl  9342  dfac8alem  9444  dfac8clem  9447  aceq3lem  9535  dfac5lem3  9540  dfac5lem4  9541  dfac5  9543  dfac2b  9545  dfac9  9551  kmlem1  9565  kmlem12  9576  kmlem14  9578  fin2i  9706  isfin2-2  9730  fin23lem21  9750  fin1a2lem10  9820  axcc2lem  9847  dominf  9856  ac5b  9889  zornn0g  9916  axdclem  9930  dominfac  9984  elwina  10097  elina  10098  iswun  10115  rankcf  10188  axrrecex  10574  elimne0  10620  1re  10630  recex  11261  xnn0nemnf  11967  uzn0  12249  qreccl  12358  xrnemnf  12502  xrnepnf  12503  xnn0n0n1ge2b  12516  fztpval  12959  expcl2lem  13431  hashnemnf  13694  hashneq0  13715  hashge2el2difr  13829  hashdmpropge2  13831  relexp1g  14375  ntrivcvgn0  15244  ntrivcvgmullem  15247  fprodntriv  15286  divalglem7  15740  divalg  15744  gcdcllem1  15838  gcdcllem3  15840  pcpre1  16169  pcqmul  16180  pcqcl  16183  prmgaplem3  16379  prmgaplem4  16380  xpsfrnel  16825  mreintcl  16856  isdrs  17534  isipodrs  17761  sgrp2rid2ex  18032  frgpuptinv  18828  isdrngrd  19459  isnzr2  19966  psgnodpmr  20664  lindfrn  20895  dmatelnd  21035  dmatmul  21036  mdetdiaglem  21137  mdetunilem1  21151  fvmptnn04ifa  21388  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  fiinopn  21439  hausnei  21866  dfconn2  21957  2ndcdisj  21994  regr1lem2  22278  isfbas  22367  ioorinv  24106  ioorcl  24107  vitalilem2  24139  vitalilem3  24140  vitali  24143  itg1climres  24244  mbfi1fseqlem4  24248  dvferm1lem  24510  dvferm2lem  24512  isuc1p  24663  ismon1p  24665  ply1remlem  24685  plydivlem4  24814  aannenlem1  24846  aannenlem2  24847  lgsne0  25839  lgsqr  25855  axtg5seg  26179  axtgupdim2  26185  axtgeucl  26186  axlowdim1  26673  lpvtx  26781  umgrnloopv  26819  usgrnloopvALT  26911  umgrvad2edg  26923  cusgrfilem2  27166  pthdlem2lem  27476  iswwlks  27542  iswwlksnx  27546  2pthdlem1  27637  isclwwlk  27690  3pthdlem1  27871  upgr3v3e3cycl  27887  upgr4cycl4dv4e  27892  eupth2lem2  27926  eupth2lem3lem4  27938  eupth2lem3lem6  27940  3cyclfrgrrn1  27992  4cycl2vnunb  27997  frgrreg  28101  norm1exi  28955  shintcl  29035  chintcl  29037  chne0  29199  elspansn2  29272  eigre  29540  eigorth  29543  kbpj  29661  superpos  30059  hatomic  30065  isprmidl  30875  xrge0iifhom  31080  xrge0iif1  31081  esumpr2  31226  sibfof  31498  signswn0  31730  signswch  31731  signstfvneq0  31742  axtgupdim2ALTV  31839  bnj168  31900  bnj970  32119  bnj1154  32169  umgracycusgr  32299  cusgracyclt3v  32301  subfacp1lem1  32324  erdszelem8  32343  indispconn  32379  cvmsss2  32419  nepss  32846  frmin  32982  elwlim  33008  nolesgn2ores  33077  nosepdmlem  33085  nosupbnd1lem3  33108  nosupbnd1lem5  33110  nosupbnd2lem1  33113  dfrdg4  33310  fvray  33500  linedegen  33502  fvline  33503  hilbert1.1  33513  rankeq1o  33530  unblimceq0lem  33743  knoppndvlem21  33769  poimirlem1  34775  poimirlem17  34791  poimirlem20  34794  poimirlem32  34806  itg2addnclem3  34827  neificl  34911  isdrngo3  35120  ispridl  35195  ismaxidl  35201  islshp  35997  lsatn0  36017  lshpset2N  36137  atlex  36334  hlsuprexch  36399  3dimlem1  36476  llni2  36530  lplni2  36555  2llnjN  36585  lvoli2  36599  2lplnj  36638  islinei  36758  lnatexN  36797  llnexchb2  36887  lhpmatb  37049  cdleme40m  37485  cdlemftr3  37583  cdlemk28-3  37926  cdlemk35s  37955  cdlemk39s  37957  cdlemk42  37959  nnn1suc  39039  dnnumch1  39524  aomclem3  39536  aomclem8  39541  dfac11  39542  dfacbasgrp  39588  dfsucon  39769  ax6e2ndeq  40773  ax6e2ndeqVD  41123  fnchoice  41166  fiiuncl  41207  disjrnmpt2  41329  idlimc  41787  limcperiod  41789  limclner  41812  cnrefiisp  41991  climxlim2lem  42006  fperdvper  42083  stoweidlem35  42201  stoweidlem43  42209  stoweidlem59  42225  fourierdlem76  42348  etransclem47  42447  nnfoctbdjlem  42618  elprneb  43145  ichexmpl1  43478  ichnreuop  43481  nrhmzr  44042  inlinecirc02plem  44671
  Copyright terms: Public domain W3C validator