MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq2 Structured version   Unicode version

Theorem eqeq2 2482
Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Assertion
Ref Expression
eqeq2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )

Proof of Theorem eqeq2
StepHypRef Expression
1 id 22 . 2  |-  ( A  =  B  ->  A  =  B )
21eqeq2d 2481 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  eqeq2i  2485  eqeq12  2486  eleq1OLD  2541  neeq2OLD  2751  alexeqg  3232  alexeq  3233  pm13.183  3244  eqeu  3274  moeq3  3280  mo2icl  3282  mob2  3283  euind  3290  reu6i  3294  reu2eqd  3300  reuind  3307  sbc2or  3340  sbc5  3356  csbiebg  3458  eqif  3977  sneq  4037  preqr1  4200  prel12  4203  preq12bg  4205  prel12g  4206  disji2  4434  disjprg  4443  dtruALT  4679  dtruALT2  4691  opth  4721  euotd  4748  solin  4823  ordequn  4978  ideqg  5154  resieq  5284  cnveqb  5462  cnveq0  5463  iota5  5571  funopg  5620  fneq2  5670  foeq3  5793  tz6.12f  5884  funbrfv  5906  fnbrfvb  5908  fvelimab  5923  elrnrexdm  6025  fconst5  6118  eufnfv  6134  f1veqaeq  6156  isosolem  6231  mpt2eq123  6340  ovmpt4g  6409  ov3  6423  ovg  6425  caovcang  6460  caovcan  6463  tfisi  6677  tfindsg  6679  findsg  6711  f1oweALT  6768  seqomlem2  7116  oawordeu  7204  omopth  7307  ereq2  7319  qsdisj  7388  eroveu  7406  2dom  7588  fundmen  7589  xpf1o  7679  nneneq  7700  cantnflem1  8108  cantnflem1OLD  8131  alephfp  8489  dfac5  8509  cardcf  8632  cfeq0  8636  sornom  8657  fpwwe2cbv  9008  fpwwe2lem3  9011  ltsosr  9471  map2psrpr  9487  axpre-lttri  9542  subval  9811  divval  10209  nn0ind-raph  10961  uzrdgfni  12037  sqeqor  12250  nn0opth2  12320  hashrabsn1  12410  elprchashprn2  12429  hashbclem  12467  hashbc  12468  hash2prde  12482  hash2pwpr  12485  wrdind  12665  wrd2ind  12666  reuccats1lem  12668  sqrtval  13033  sqrmo  13048  summolem2  13501  divides  13849  dvdstr  13878  odd2np1lem  13904  ndvdssub  13924  bitsinv1  13951  eucalglt  14073  ramcl2lem  14386  ramcl  14406  cshwrepswhash1  14445  imasaddfnlem  14783  posi  15437  orbsta  16156  symgfvne  16218  symgfix2  16246  odlem1  16365  gexlem1  16405  slwispgp  16437  sylow3lem6  16458  efgrelexlemb  16574  gsumval3OLD  16711  gsumval3lem2  16713  pgpfac1  16933  pgpfaclem2  16935  pgpfac  16937  ablfaclem1  16938  isdomn  17742  mvrval  17876  coe1tmmul2  18116  coe1tmmul  18117  obsip  18547  uvcval  18611  mat1comp  18737  mat1dimid  18771  scmateALT  18809  marrepval  18859  marepvval  18864  minmar1val  18945  gsummatr01  18956  t0sep  19619  t1sep2  19664  is2ndc  19741  kqt0lem  20000  isr0  20001  isufil2  20172  xmeteq0  20604  imasf1oxmet  20641  xrsxmet  21077  iccpnfcnv  21207  dyadmax  21770  dyadmbl  21772  dvfsumle  22185  dvfsumabs  22187  dvfsumlem1  22190  mdegle0  22240  fta1g  22331  ig1peu  22335  fta1  22466  aalioulem2  22491  efopn  22795  efrlim  23055  musum  23223  dvdsmulf1o  23226  dchrsum2  23299  sumdchr2  23301  axtgcgrid  23616  axtgbtwnid  23619  tglowdim1i  23648  islmib  23858  axcontlem12  23982  wlkon  24237  wlkntrllem3  24267  spthonepeq  24293  fargshiftf1  24341  constr3trllem2  24355  wlklniswwlkn2  24404  usg2wlkeq  24412  wwlknredwwlkn  24430  wwlkextprop  24448  clwwlkn  24471  clwlkisclwwlklem2a4  24488  clwwlkext2edg  24506  clwwnisshclwwn  24513  hashecclwwlkn1  24538  usghashecclwwlk  24539  clwlkfoclwwlk  24549  2wlkonot  24569  2spthonot  24570  el2wlkonot  24573  el2spthonot  24574  el2spthonot0  24575  rusgraprop2  24646  rusgrasn  24649  rusgranumwlklem1  24653  rusgranumwlklem2  24654  rusgranumwlklem3  24655  rusgranumwlkg  24662  clwlknclwlkdifs  24664  frgra3vlem1  24704  3vfriswmgralem  24708  usg2spot2nb  24770  usgreg2spot  24772  2spotmdisj  24773  usgreghash2spot  24774  numclwwlkdisj  24785  numclwwlkovf  24786  numclwwlkovg  24792  numclwlk1lem2f1  24799  numclwwlkovq  24804  numclwwlkovh  24806  numclwwlk5  24817  frgrareg  24822  frgraregord013  24823  friendshipgt3  24826  ex-opab  24858  isgrpoi  24904  grpoidinv2  24924  isgrp2d  24941  isgrpda  25003  isexid2  25031  ghgrp  25074  hvsubeq0  25689  hvaddcan  25691  hvsubadd  25698  normsub0  25757  omlsi  26026  pjoml  26058  nonbooli  26273  pj11  26336  lnopeq  26632  nmopun  26637  pjclem4a  26821  pj3lem1  26829  strlem4  26877  hstrlem4  26885  jplem1  26891  superpos  26977  rmoeq  27090  ifeqeqx  27121  disji2f  27139  disjif2  27143  disjabrex  27144  disjabrexf  27145  disjxpin  27148  disjunsn  27154  ofpreima  27207  fgreu  27213  fcnvgreu  27214  xrge0iifcnv  27579  esumpr2  27742  eulerpartlemgvv  27983  eulerpartlemgh  27985  eulerpartlemgs2  27987  sgnsub  28151  plymulx0  28172  subfacp1lem3  28294  pconcn  28337  cnpcon  28343  txpcon  28345  conpcon  28348  cvmlift3lem2  28433  cvmlift3lem4  28435  cvmlift3  28441  snmlflim  28445  ghomf1olem  28537  relexpindlem  28565  iota5f  28605  prodmolem2  28672  sltres  29029  nofulllem5  29071  rankeq1o  29433  fin2so  29645  mblfinlem2  29657  mbfresfi  29666  cnambfre  29668  ftc1anclem8  29702  nn0prpw  29746  f1opr  29846  fdc  29869  istotbnd  29896  ismaxidl  30068  mpt2bi123f  30203  mptbi12f  30207  unxpwdom3  30673  dgraalem  30727  dgraaub  30730  hashgcdeq  30791  pm13.192  30923  2sbc6g  30928  2sbc5g  30929  pm14.122b  30936  dirkertrigeqlem3  31428  fourierdlem42  31477  equncomVD  32766  csbingVD  32782  csbsngVD  32791  csbxpgVD  32792  csbresgVD  32793  csbrngVD  32794  csbima12gALTVD  32795  csbunigVD  32796  csbfv12gALTVD  32797  relopabVD  32799  bnj1321  33180  bj-csbsnlem  33569  lsatcmp  33818  lshpkrlem1  33925  trlval2  34977  cdlemg1cex  35402  cdlemm10N  35933  dicval  35991
  Copyright terms: Public domain W3C validator