Theorem eqeq2 2816

Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Assertion

Ref	Expression
eqeq2	⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Proof of Theorem eqeq2

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq2d 2815	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2798

This theorem is referenced by:  eqeq2i  2817  eqeq12  2818  alexeqg  3525  clel5  3537  pm13.183  3538  eqeu  3572  moeq3  3578  mo2icl  3580  mob2  3581  euind  3588  reu6i  3592  reu2eqd  3598  reuind  3606  sbc2or  3639  sbc5  3655  csbiebg  3748  eqif  4316  sneq  4377  preq1b  4561  prel12OLD  4566  preq12bg  4569  prel12gOLD  4570  preqsn  4579  preqsnOLD  4580  disji2  4824  disjprg  4836  dtruALT  5054  dtruALT2  5098  opth  5131  euotd  5165  solin  5252  ideqg  5472  resieq  5608  cnveqb  5798  cnveq0  5799  iota5  6081  funopg  6132  fneq2  6188  foeq3  6326  tz6.12f  6429  funbrfv  6451  fnbrfvb  6453  fvelimab  6471  elrnrexdm  6582  funsndifnop  6637  fconst5  6693  eufnfv  6713  f1veqaeq  6735  fpropnf1  6745  isosolem  6818  mpt2eq123  6941  ovmpt4g  7010  ov3  7024  ovg  7026  caovcang  7062  caovcan  7065  tfisi  7285  tfindsg  7287  findsg  7320  f1oweALT  7379  seqomlem2  7779  oawordeu  7869  omopth  7972  ereq2  7984  qsdisj  8056  eroveu  8075  2dom  8262  fundmen  8263  xpf1o  8358  nneneq  8379  cantnflem1  8830  updjud  9040  alephfp  9211  dfac5  9231  cardcf  9356  cfeq0  9360  sornom  9381  fpwwe2cbv  9734  fpwwe2lem3  9737  ltsosr  10197  map2psrpr  10213  axpre-lttri  10268  subval  10554  divval  10969  nn0ind-raph  11739  uzrdgfni  12977  sqeqor  13197  nn0opth2  13275  hashrabsn1  13377  elprchashprn2  13397  hashbclem  13449  hashbc  13450  hash2prde  13465  hash2pwpr  13471  brfi1indALT  13495  wrdind  13696  wrd2ind  13697  reuccats1lem  13699  cshf1  13776  wrdl3s3  13926  relexpindlem  14022  sqrtval  14196  sqrmo  14211  summolem2  14666  prodmolem2  14882  divides  15201  dvdstr  15237  odd2np1lem  15280  ndvdssub  15348  bitsinv1  15379  eucalglt  15513  hashgcdeq  15707  ramcl2lem  15926  ramcl  15946  cshwrepswhash1  16017  imasaddfnlem  16389  fnhomeqhomf  16551  initoeu2lem1  16864  posi  17151  sgrp2nmndlem3  17613  dfgrp2  17648  grpidinv  17676  dfgrp3lem  17714  orbsta  17943  symgfvne  18005  symgfix2  18033  odlem1  18151  gexlem1  18191  slwispgp  18223  sylow3lem6  18244  efgrelexlemb  18360  gsumval3lem2  18504  pgpfac1  18677  pgpfaclem2  18679  pgpfac  18681  ablfaclem1  18682  isdomn  19499  mvrval  19626  coe1tmmul2  19850  coe1tmmul  19851  obsip  20271  uvcval  20330  mat1comp  20452  mat1dimid  20487  scmateALT  20525  marrepval  20575  marepvval  20580  minmar1val  20661  gsummatr01  20673  t0sep  21338  t1sep2  21383  is2ndc  21459  kqt0lem  21749  isr0  21750  isufil2  21921  xmeteq0  22352  imasf1oxmet  22389  xrsxmet  22821  iccpnfcnv  22952  dyadmax  23575  dyadmbl  23577  dvfsumle  23994  dvfsumabs  23996  dvfsumlem1  23999  mdegle0  24047  fta1g  24137  ig1peu  24141  fta1  24273  aalioulem2  24298  efopn  24614  efrlim  24906  musum  25127  dvdsmulf1o  25130  dchrsum2  25203  sumdchr2  25205  gausslemma2dlem0i  25299  axtgcgrid  25572  axtgbtwnid  25575  tglowdim1i  25606  islmib  25889  axcontlem12  26065  upgredgpr  26248  ushgredgedg  26332  ushgredgedgloop  26334  ushgredgedgloopOLD  26335  rusgrpropnb  26703  rgrx0ndm  26713  uspgr2wlkeq  26766  wlkson  26776  upgrwlkdvdelem  26856  spthonepeq  26872  iswwlksnon  26971  iswwlksnonOLD  26972  wlklnwwlkln2lem  27005  wwlksnredwwlkn  27028  wwlksnextprop  27046  wwlksnwwlksnon  27049  wwlksnwwlksnonOLD  27051  elwwlks2ons3  27091  elwwlks2ons3OLD  27092  rusgrnumwwlklem  27108  clwwlknclwwlkdifsOLD  27118  clwlkclwwlklem2a4  27136  clwwlkn  27167  clwwlknOLD  27168  clwwlkext2edg  27202  hashecclwwlkn1  27224  umgrhashecclwwlk  27225  clwlksfoclwwlkOLD  27233  clwwlknon  27251  clwwlknonOLD  27252  clwwlk0on0  27255  clwwlknondisjOLD  27281  uhgr3cyclexlem  27350  1conngr  27363  frgr3vlem1  27444  3vfriswmgrlem  27448  frgrwopreglem3  27485  fusgreg2wsplem  27504  fusgreghash2wsp  27509  numclwwlkovgOLD  27524  numclwlk1lem1  27545  numclwwlkovq  27550  numclwwlk2lem1  27552  numclwwlkovhOLD  27558  numclwwlk2lem1OLD  27559  frgrregord013  27579  friendshipgt3  27582  ex-opab  27616  isgrpoi  27677  grpoidinv2  27694  hvsubeq0  28250  hvaddcan  28252  hvsubadd  28259  normsub0  28318  omlsi  28588  pjoml  28620  nonbooli  28835  pj11  28898  lnopeq  29193  nmopun  29198  pjclem4a  29382  pj3lem1  29390  strlem4  29438  hstrlem4  29446  jplem1  29452  superpos  29538  ifeqeqx  29683  disji2f  29712  disjif2  29716  disjabrex  29717  disjabrexf  29718  disjxpin  29723  disjunsn  29729  ofpreima  29789  fgreu  29795  fcnvgreu  29796  xrge0iifcnv  30301  esumpr2  30451  eulerpartlemgvv  30760  eulerpartlemgh  30762  eulerpartlemgs2  30764  sgnsub  30928  plymulx0  30946  bnj1321  31415  subfacp1lem3  31484  pconncn  31526  cnpconn  31532  txpconn  31534  connpconn  31537  cvmlift3lem2  31622  cvmlift3lem4  31624  cvmlift3  31630  snmlflim  31634  iota5f  31925  br1steqgOLD  31991  br2ndeqgOLD  31992  sltres  32133  noprefixmo  32166  nosupno  32167  nosupfv  32170  rankeq1o  32596  nn0prpw  32636  bj-csbsnlem  33203  bj-restsnss  33344  bj-restsnss2  33345  fin2so  33706  poimirlem2  33721  poimirlem18  33737  poimirlem21  33740  poimirlem25  33744  poimirlem26  33745  poimirlem27  33746  mblfinlem2  33757  mbfresfi  33765  cnambfre  33767  ftc1anclem8  33801  f1opr  33828  fdc  33849  istotbnd  33876  isexid2  33962  isgrpda  34062  ismaxidl  34147  mpt2bi123f  34278  mptbi12f  34282  lsatcmp  34780  lshpkrlem1  34887  trlval2  35941  cdlemg1cex  36366  cdlemm10N  36896  dicval  36954  unxpwdom3  38163  dgraalem  38213  dgraaub  38216  frege104  38758  pm13.192  39107  2sbc6g  39112  2sbc5g  39113  pm14.122b  39120  equncomVD  39595  csbingVD  39611  csbsngVD  39620  csbxpgVD  39621  csbresgVD  39622  csbrngVD  39623  csbima12gALTVD  39624  csbunigVD  39625  csbfv12gALTVD  39626  relopabVD  39628  dvnprodlem1  40638  dvnprodlem2  40639  dvnprodlem3  40640  dvnprod  40641  fourierdlem42  40842  etransclem11  40938  etransclem12  40939  etransclem33  40960  nnfoctbdjlem  41148  hoimbl  41324  aiota0def  41675  funressndmafv2rn  41809  funressnbrafv2  41830  dfatbrafv2b  41831  funbrafv2  41833  fnbrafv2b  41834  fargshiftf1  41949  reuccatpfxs1lem  42005  uspgrsprf1  42320  uspgrsprfo  42321  lidldomn1  42486  nn0sumshdiglem2  42981  setrec2lem2  43006