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

Theorem eqeq2 2472
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 2471 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-cleq 2454
This theorem is referenced by:  eqeq2i  2473  eqeq12  2474  alexeqg  3179  pm13.183  3190  eqeu  3220  moeq3  3226  mo2icl  3228  mob2  3229  euind  3236  reu6i  3240  reu2eqd  3246  reuind  3254  sbc2or  3287  sbc5  3303  csbiebg  3397  eqif  3930  sneq  3989  preq1b  4158  preqr1OLD  4161  prel12  4164  preq12bg  4167  prel12g  4168  disji2  4402  disjprg  4411  dtruALT  4645  dtruALT2  4657  opth  4689  euotd  4715  solin  4796  ideqg  5004  resieq  5133  cnveqb  5309  cnveq0  5310  ordequn  5541  iota5  5584  funopg  5632  fneq2  5686  foeq3  5813  tz6.12f  5905  funbrfv  5925  fnbrfvb  5927  fvelimab  5943  elrnrexdm  6048  fconst5  6145  eufnfv  6163  f1veqaeq  6185  isosolem  6262  mpt2eq123  6376  ovmpt4g  6445  ov3  6459  ovg  6461  caovcang  6496  caovcan  6499  tfisi  6711  tfindsg  6713  findsg  6746  f1oweALT  6803  seqomlem2  7193  oawordeu  7281  omopth  7384  ereq2  7396  qsdisj  7465  eroveu  7483  2dom  7667  fundmen  7668  xpf1o  7759  nneneq  7780  cantnflem1  8219  alephfp  8564  dfac5  8584  cardcf  8707  cfeq0  8711  sornom  8732  fpwwe2cbv  9080  fpwwe2lem3  9083  ltsosr  9543  map2psrpr  9559  axpre-lttri  9614  subval  9891  divval  10299  nn0ind-raph  11063  uzrdgfni  12203  sqeqor  12419  nn0opth2  12489  hashrabsn1  12584  elprchashprn2  12604  hashbclem  12647  hashbc  12648  hash2prde  12663  hash2pwpr  12667  brfi1indALT  12685  wrdind  12869  wrd2ind  12870  reuccats1lem  12872  relexpindlem  13174  sqrtval  13348  sqrmo  13363  summolem2  13830  prodmolem2  14037  divides  14355  dvdstr  14385  odd2np1lem  14412  ndvdssub  14436  bitsinv1  14464  eucalglt  14592  ramcl2lem  15010  ramcl2lemOLD  15011  ramcl  15035  cshwrepswhash1  15121  imasaddfnlem  15482  fnhomeqhomf  15644  initoeu2lem1  15957  posi  16243  sgrp2nmndlem3  16707  orbsta  17015  symgfvne  17077  symgfix2  17105  odlem1  17229  odlem1OLD  17232  gexlem1  17276  gexlem1OLD  17278  slwispgp  17311  sylow3lem6  17332  efgrelexlemb  17448  gsumval3lem2  17588  pgpfac1  17761  pgpfaclem2  17763  pgpfac  17765  ablfaclem1  17766  isdomn  18566  mvrval  18693  coe1tmmul2  18917  coe1tmmul  18918  obsip  19332  uvcval  19391  mat1comp  19513  mat1dimid  19547  scmateALT  19585  marrepval  19635  marepvval  19640  minmar1val  19721  gsummatr01  19732  t0sep  20388  t1sep2  20433  is2ndc  20509  kqt0lem  20799  isr0  20800  isufil2  20971  xmeteq0  21401  imasf1oxmet  21438  xrsxmet  21875  iccpnfcnv  22020  dyadmax  22604  dyadmbl  22606  dvfsumle  23021  dvfsumabs  23023  dvfsumlem1  23026  mdegle0  23074  fta1g  23166  ig1peu  23170  ig1peuOLD  23171  fta1  23309  aalioulem2  23337  efopn  23651  efrlim  23943  musum  24168  dvdsmulf1o  24171  dchrsum2  24244  sumdchr2  24246  axtgcgrid  24559  axtgbtwnid  24562  tglowdim1i  24593  islmib  24877  axcontlem12  25053  wlkon  25309  wlkntrllem3  25339  spthonepeq  25365  fargshiftf1  25413  constr3trllem2  25427  wlklniswwlkn2  25476  usg2wlkeq  25484  wwlknredwwlkn  25502  wwlkextprop  25520  clwwlkn  25543  clwlkisclwwlklem2a4  25560  clwwlkext2edg  25578  clwwnisshclwwn  25585  hashecclwwlkn1  25610  usghashecclwwlk  25611  clwlkfoclwwlk  25621  2wlkonot  25641  2spthonot  25642  el2wlkonot  25645  el2spthonot  25646  el2spthonot0  25647  rusgraprop2  25718  rusgrasn  25721  rusgranumwlklem1  25725  rusgranumwlklem2  25726  rusgranumwlklem3  25727  rusgranumwlkg  25734  clwlknclwlkdifs  25736  frgra3vlem1  25776  3vfriswmgralem  25780  usg2spot2nb  25841  usgreg2spot  25843  2spotmdisj  25844  usgreghash2spot  25845  numclwwlkdisj  25856  numclwwlkovf  25857  numclwwlkovg  25863  numclwlk1lem2f1  25870  numclwwlkovq  25875  numclwwlkovh  25877  numclwwlk5  25888  frgrareg  25893  frgraregord013  25894  friendshipgt3  25897  ex-opab  25930  isgrpoi  25974  grpoidinv2  25994  isgrp2d  26011  isgrpda  26073  isexid2  26101  ghgrpOLD  26144  hvsubeq0  26769  hvaddcan  26771  hvsubadd  26778  normsub0  26837  omlsi  27105  pjoml  27137  nonbooli  27352  pj11  27415  lnopeq  27710  nmopun  27715  pjclem4a  27899  pj3lem1  27907  strlem4  27955  hstrlem4  27963  jplem1  27969  superpos  28055  rmoeqALT  28171  ifeqeqx  28206  disji2f  28235  disjif2  28239  disjabrex  28240  disjabrexf  28241  disjxpin  28246  disjunsn  28252  ofpreima  28316  fgreu  28322  fcnvgreu  28323  xrge0iifcnv  28787  esumpr2  28936  eulerpartlemgvv  29257  eulerpartlemgh  29259  eulerpartlemgs2  29261  sgnsub  29463  plymulx0  29484  bnj1321  29884  subfacp1lem3  29953  pconcn  29995  cnpcon  30001  txpcon  30003  conpcon  30006  cvmlift3lem2  30091  cvmlift3lem4  30093  cvmlift3  30099  snmlflim  30103  ghomf1olem  30360  iota5f  30405  br1steqg  30464  br2ndeqg  30465  sltres  30599  nofulllem5  30643  rankeq1o  30986  nn0prpw  31027  bj-csbsnlem  31549  fin2so  31976  poimirlem2  31986  poimirlem18  32002  poimirlem21  32005  poimirlem25  32009  poimirlem26  32010  poimirlem27  32011  mblfinlem2  32022  mbfresfi  32031  cnambfre  32033  ftc1anclem8  32068  f1opr  32095  fdc  32118  istotbnd  32145  ismaxidl  32317  mpt2bi123f  32450  mptbi12f  32454  lsatcmp  32613  lshpkrlem1  32720  trlval2  33773  cdlemg1cex  34199  cdlemm10N  34730  dicval  34788  unxpwdom3  35997  dgraalem  36051  dgraalemOLD  36052  dgraaub  36057  dgraaubOLD  36058  hashgcdeq  36119  frege104  36607  pm13.192  36804  2sbc6g  36809  2sbc5g  36810  pm14.122b  36817  equncomVD  37304  csbingVD  37320  csbsngVD  37329  csbxpgVD  37330  csbresgVD  37331  csbrngVD  37332  csbima12gALTVD  37333  csbunigVD  37334  csbfv12gALTVD  37335  relopabVD  37337  disjinfi  37505  dvnprodlem1  37858  dvnprodlem2  37859  dvnprodlem3  37860  dvnprod  37861  fourierdlem42  38049  fourierdlem42OLD  38050  etransclem11  38147  etransclem12  38148  etransclem33  38169  nnfoctbdjlem  38330  hoimbl  38490  reuccatpfxs1lem  39013  clel5  39020  funsndifnop  39063  fundmge2nop  39067  fpropnf1  39077  upgredgpr  39279  ushgredgedga  39355  ushgredgedgaloop  39357  rusgrpropnb  39648  rgrx0ndm  39657  wlkson  39706  upgrwlkdvdelem  39767  spthonepeq-av  39783  uhgr3cyclexlem  39921  1conngr  39934  lidldomn1  40193  nn0sumshdiglem2  40705
  Copyright terms: Public domain W3C validator