Theorem eqeq2 2833

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 2832	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  eqeq2i  2834  eqeq12  2835  alexeqg  3643  clel5OLD  3657  pm13.183  3658  pm13.183OLD  3659  eqeu  3696  moeq3  3702  mo2icl  3704  mob2  3705  euind  3714  reu6i  3718  reu2eqd  3726  reuind  3743  sbc2or  3780  sbc5  3799  csbiebg  3914  eqif  4506  sneq  4570  reusngf  4605  rexreusng  4610  reuprg0  4631  preq1b  4770  preq12bg  4777  preqsn  4785  disji2  5040  disjprgw  5053  disjprg  5054  dtruALT  5280  dtruALT2  5327  opth  5360  euotd  5395  solin  5492  ideqg  5716  resieq  5858  cnveqb  6047  cnveq0  6048  reu3op  6137  reuop  6138  iota5  6332  funopg  6383  fneq2  6439  foeq3  6582  tz6.12f  6688  funbrfv  6710  fnbrfvb  6712  fvelimab  6731  elrnrexdm  6849  funsndifnop  6907  fconst5  6962  eufnfv  6985  f1veqaeq  7009  fpropnf1  7019  nf1const  7053  isosolem  7094  f1opr  7204  mpoeq123  7220  ovmpt4g  7291  ov3  7305  ovg  7307  caovcang  7343  caovcan  7346  tfisi  7567  tfindsg  7569  findsg  7603  f1oweALT  7667  seqomlem2  8081  oawordeu  8175  omopth  8279  ereq2  8291  qsdisj  8368  eroveu  8386  2dom  8576  fundmen  8577  xpf1o  8673  nneneq  8694  cantnflem1  9146  updjud  9357  alephfp  9528  dfac5  9548  cardcf  9668  cfeq0  9672  sornom  9693  fpwwe2cbv  10046  fpwwe2lem3  10049  ltsosr  10510  map2psrpr  10526  axpre-lttri  10581  subval  10871  divval  11294  nn0ind-raph  12076  uzrdgfni  13320  sqeqor  13572  nn0opth2  13626  hashrabsn1  13729  elprchashprn2  13751  hashbclem  13804  hashbc  13805  hash2prde  13822  hash2pwpr  13828  brfi1indALT  13852  wrdind  14078  wrd2ind  14079  reuccatpfxs1lem  14102  cshf1  14166  wrdl3s3  14320  relexpindlem  14416  sqrtval  14590  sqrmo  14605  reusq0  14816  summolem2  15067  prodmolem2  15283  divides  15603  dvdstr  15640  odd2np1lem  15683  ndvdssub  15754  bitsinv1  15785  eucalglt  15923  hashgcdeq  16120  ramcl2lem  16339  ramcl  16359  cshwrepswhash1  16430  imasaddfnlem  16795  fnhomeqhomf  16955  initoeu2lem1  17268  posi  17554  sgrp2nmndlem3  18084  dfgrp2  18122  grpidinv  18153  dfgrp3lem  18191  orbsta  18437  symgfvne  18503  symgfix2  18538  odlem1  18657  gexlem1  18698  slwispgp  18730  sylow3lem6  18751  efgrelexlemb  18870  gsumval3lem2  19020  pgpfac1  19196  pgpfaclem2  19198  pgpfac  19200  ablfaclem1  19201  isdomn  20061  mvrval  20195  mhpval  20327  coe1tmmul2  20438  coe1tmmul  20439  obsip  20859  uvcval  20923  mat1comp  21043  mat1dimid  21077  scmateALT  21115  marrepval  21165  marepvval  21170  minmar1val  21251  gsummatr01  21262  t0sep  21926  t1sep2  21971  is2ndc  22048  kqt0lem  22338  isr0  22339  isufil2  22510  xmeteq0  22942  imasf1oxmet  22979  xrsxmet  23411  iccpnfcnv  23542  dyadmax  24193  dyadmbl  24195  dvfsumle  24612  dvfsumabs  24614  dvfsumlem1  24617  mdegle0  24665  fta1g  24755  ig1peu  24759  fta1  24891  aalioulem2  24916  efopn  25235  efrlim  25541  musum  25762  dvdsmulf1o  25765  dchrsum2  25838  sumdchr2  25840  gausslemma2dlem0i  25934  addsqnreup  26013  2sqreulem1  26016  2sqreultblem  26018  2sqreunnlem1  26019  2sqreunnltblem  26021  2sqreulem3  26023  axtgcgrid  26243  axtgbtwnid  26246  tglowdim1i  26281  islmib  26567  axcontlem12  26755  upgredgpr  26921  ushgredgedg  27005  ushgredgedgloop  27007  rusgrpropnb  27359  rgrx0ndm  27369  uspgr2wlkeq  27421  wlkson  27432  upgrwlkdvdelem  27511  spthonepeq  27527  iswwlksnon  27625  wlklnwwlkln2lem  27654  wwlksnredwwlkn  27667  wwlksnextprop  27685  wwlksnwwlksnon  27688  elwwlks2ons3  27728  rusgrnumwwlklem  27743  clwlkclwwlklem2a4  27769  clwwlkn  27798  clwwlkext2edg  27829  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  clwwlknon  27863  clwwlk0on0  27865  uhgr3cyclexlem  27954  1conngr  27967  frgr3vlem1  28046  3vfriswmgrlem  28050  frgrwopreglem3  28087  fusgreg2wsplem  28106  fusgreghash2wsp  28111  numclwlk1lem1  28142  numclwwlkovq  28147  numclwwlk2lem1  28149  frgrregord013  28168  friendshipgt3  28171  ex-opab  28205  isgrpoi  28269  grpoidinv2  28286  hvsubeq0  28839  hvaddcan  28841  hvsubadd  28848  normsub0  28907  omlsi  29175  pjoml  29207  nonbooli  29422  pj11  29485  lnopeq  29780  nmopun  29785  pjclem4a  29969  pj3lem1  29977  strlem4  30025  hstrlem4  30033  jplem1  30039  superpos  30125  ifeqeqx  30291  disji2f  30321  disjif2  30325  disjabrex  30326  disjabrexf  30327  disjxpin  30332  disjunsn  30338  ofpreima  30404  fgreu  30411  fcnvgreu  30412  ismxidl  30966  xrge0iifcnv  31171  esumpr2  31321  eulerpartlemgvv  31629  eulerpartlemgh  31631  eulerpartlemgs2  31633  sgnsub  31797  plymulx0  31812  lpadmax  31948  lpadright  31950  bnj1321  32294  f1resfz0f1d  32356  subfacp1lem3  32424  pconncn  32466  cnpconn  32472  txpconn  32474  connpconn  32477  cvmlift3lem2  32562  cvmlift3lem4  32564  cvmlift3  32570  snmlflim  32574  iota5f  32950  sltres  33164  noprefixmo  33197  nosupno  33198  nosupfv  33201  rankeq1o  33627  nn0prpw  33666  bj-csbsnlem  34215  bj-restsnss  34368  bj-restsnss2  34369  fin2so  34873  poimirlem2  34888  poimirlem18  34904  poimirlem21  34907  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  mblfinlem2  34924  mbfresfi  34932  cnambfre  34934  ftc1anclem8  34968  fdc  35014  istotbnd  35041  isexid2  35127  isgrpda  35227  ismaxidl  35312  mpobi123f  35434  mptbi12f  35438  qsdisjALTV  35844  lsatcmp  36133  lshpkrlem1  36240  trlval2  37293  cdlemg1cex  37718  cdlemm10N  38248  dicval  38306  nnn1suc  39152  resubval  39190  unxpwdom3  39688  dgraalem  39738  dgraaub  39741  frege104  40306  pm13.192  40735  2sbc6g  40740  2sbc5g  40741  pm14.122b  40748  equncomVD  41195  csbingVD  41211  csbsngVD  41220  csbxpgVD  41221  csbresgVD  41222  csbrngVD  41223  csbima12gALTVD  41224  csbunigVD  41225  csbfv12gALTVD  41226  relopabVD  41228  dvnprodlem1  42224  dvnprodlem2  42225  dvnprodlem3  42226  dvnprod  42227  fourierdlem42  42428  etransclem11  42524  etransclem12  42525  etransclem33  42546  nnfoctbdjlem  42731  hoimbl  42907  aiota0def  43288  euoreqb  43302  funressndmafv2rn  43416  funressnbrafv2  43437  dfatbrafv2b  43438  funbrafv2  43440  fnbrafv2b  43441  elsetpreimafvbi  43545  elsetpreimafveq  43551  imasetpreimafvbijlemfo  43559  fargshiftf1  43595  ichnreuop  43628  paireqne  43667  reupr  43678  uspgrsprf1  44016  uspgrsprfo  44017  lidldomn1  44186  nn0sumshdiglem2  44676  setrec2lem2  44791