Theorem eqeq2 2745

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqeq2i  2746  eqeq12OLD  2752  eqtr3  2759  clelab  2880  alexeqg  3640  pm13.183  3657  elab6g  3660  eqeu  3703  moeq3  3709  mo2icl  3711  mob2  3712  euind  3721  reu6i  3725  reu2eqd  3733  reuind  3750  sbc2or  3787  sbc5ALT  3807  csbiebg  3927  eqif  4570  sneq  4639  reusngf  4677  rexreusng  4684  reuprg0  4707  preq1b  4848  preq12bg  4855  preqsn  4863  disji2  5131  disjprgw  5144  disjprg  5145  dtruALT  5387  opth  5477  euotd  5514  solin  5614  ideqg  5852  resieq  5993  cnveqb  6196  cnveq0  6197  reu3op  6292  reuop  6293  iota5  6527  funopg  6583  fneq2  6642  foeq3  6804  tz6.12f  6918  funbrfv  6943  fnbrfvb  6945  fvelimab  6965  elrnrexdm  7091  funsndifnop  7149  fconst5  7207  eufnfv  7231  f1veqaeq  7256  fpropnf1  7266  nf1const  7302  isosolem  7344  f1opr  7465  mpoeq123  7481  ovmpt4g  7555  ov3  7570  ovg  7572  caovcang  7608  caovcan  7611  tfisi  7848  tfindsg  7850  findsg  7890  f1oweALT  7959  seqomlem2  8451  oawordeu  8555  omopth  8661  ereq2  8711  qsdisj  8788  eroveu  8806  2dom  9030  fundmen  9031  xpf1o  9139  pwfir  9176  nneneq  9209  nneneqOLD  9221  cantnflem1  9684  brttrcl  9708  ttrcltr  9711  ttrclss  9715  ttrclselem2  9721  updjud  9929  alephfp  10103  dfac5  10123  cardcf  10247  cfeq0  10251  sornom  10272  fpwwe2cbv  10625  fpwwe2lem3  10628  ltsosr  11089  map2psrpr  11105  axpre-lttri  11160  subval  11451  divval  11874  nn0ind-raph  12662  uzrdgfni  13923  sqeqor  14180  nn0opth2  14232  hashrabsn1  14334  elprchashprn2  14356  hashbclem  14411  hashbc  14412  hash2prde  14431  hash2pwpr  14437  brfi1indALT  14461  wrdind  14672  wrd2ind  14673  reuccatpfxs1lem  14696  cshf1  14760  wrdl3s3  14913  relexpindlem  15010  sqrtval  15184  sqrmo  15198  reusq0  15409  summolem2  15662  prodmolem2  15879  divides  16199  dvdstr  16237  odd2np1lem  16283  ndvdssub  16352  bitsinv1  16383  eucalglt  16522  hashgcdeq  16722  ramcl2lem  16942  ramcl  16962  cshwrepswhash1  17036  imasaddfnlem  17474  fnhomeqhomf  17635  initoeu2lem1  17964  cat1lem  18046  posi  18270  sgrp2nmndlem3  18806  dfgrp2  18847  grpidinv  18883  dfgrp3lem  18921  orbsta  19177  symgfvne  19248  symgfix2  19284  odlem1  19403  gexlem1  19447  slwispgp  19479  sylow3lem6  19500  efgrelexlemb  19618  gsumval3lem2  19774  pgpfac1  19950  pgpfaclem2  19952  pgpfac  19954  ablfaclem1  19955  isdomn  20910  isdomn4  20918  obsip  21276  uvcval  21340  mvrval  21541  mhpval  21683  coe1tmmul2  21798  coe1tmmul  21799  mat1comp  21942  mat1dimid  21976  scmateALT  22014  marrepval  22064  marepvval  22069  minmar1val  22150  gsummatr01  22161  t0sep  22828  t1sep2  22873  is2ndc  22950  kqt0lem  23240  isr0  23241  isufil2  23412  xmeteq0  23844  imasf1oxmet  23881  xrsxmet  24325  iccpnfcnv  24460  dyadmax  25115  dyadmbl  25117  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  mdegle0  25595  fta1g  25685  ig1peu  25689  fta1  25821  aalioulem2  25846  efopn  26166  efrlim  26474  musum  26695  dvdsmulf1o  26698  dchrsum2  26771  sumdchr2  26773  gausslemma2dlem0i  26867  addsqnreup  26946  2sqreulem1  26949  2sqreultblem  26951  2sqreunnlem1  26952  2sqreunnltblem  26954  2sqreulem3  26956  sltres  27165  nosupprefixmo  27203  noinfprefixmo  27204  nosupcbv  27205  nosupno  27206  nosupfv  27209  noinfcbv  27220  noinfno  27221  noinffv  27224  elmade  27362  divsval  27637  axtgcgrid  27714  axtgbtwnid  27717  tglowdim1i  27752  islmib  28038  axcontlem12  28233  upgredgpr  28402  ushgredgedg  28486  ushgredgedgloop  28488  rusgrpropnb  28840  rgrx0ndm  28850  uspgr2wlkeq  28903  wlkson  28913  upgrwlkdvdelem  28993  spthonepeq  29009  iswwlksnon  29107  wlklnwwlkln2lem  29136  wwlksnredwwlkn  29149  wwlksnextprop  29166  wwlksnwwlksnon  29169  elwwlks2ons3  29209  rusgrnumwwlklem  29224  clwlkclwwlklem2a4  29250  clwwlkn  29279  clwwlkext2edg  29309  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  clwwlknon  29343  clwwlk0on0  29345  uhgr3cyclexlem  29434  1conngr  29447  frgr3vlem1  29526  3vfriswmgrlem  29530  frgrwopreglem3  29567  fusgreg2wsplem  29586  fusgreghash2wsp  29591  numclwlk1lem1  29622  numclwwlkovq  29627  numclwwlk2lem1  29629  frgrregord013  29648  friendshipgt3  29651  ex-opab  29685  isgrpoi  29751  grpoidinv2  29768  hvsubeq0  30321  hvaddcan  30323  hvsubadd  30330  normsub0  30389  omlsi  30657  pjoml  30689  nonbooli  30904  pj11  30967  lnopeq  31262  nmopun  31267  pjclem4a  31451  pj3lem1  31459  strlem4  31507  hstrlem4  31515  jplem1  31521  superpos  31607  ifeqeqx  31774  disji2f  31808  disjif2  31812  disjabrex  31813  disjabrexf  31814  disjxpin  31819  disjunsn  31825  ofpreima  31890  fgreu  31897  fcnvgreu  31898  gsumhashmul  32208  domnlcan  32376  ismxidl  32578  xrge0iifcnv  32913  esumpr2  33065  eulerpartlemgvv  33375  eulerpartlemgh  33377  eulerpartlemgs2  33379  sgnsub  33543  plymulx0  33558  lpadmax  33694  lpadright  33696  bnj1321  34038  f1resfz0f1d  34103  subfacp1lem3  34173  pconncn  34215  cnpconn  34221  txpconn  34223  connpconn  34226  cvmlift3lem2  34311  cvmlift3lem4  34313  cvmlift3  34319  snmlflim  34323  iota5f  34693  rankeq1o  35143  gg-dvfsumle  35182  nn0prpw  35208  bj-csbsnlem  35783  bj-elgab  35819  bj-restsnss  35964  bj-restsnss2  35965  bj-imdirco  36071  fin2so  36475  poimirlem2  36490  poimirlem18  36506  poimirlem21  36509  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  mblfinlem2  36526  mbfresfi  36534  cnambfre  36536  ftc1anclem8  36568  fdc  36613  istotbnd  36637  isexid2  36723  isgrpda  36823  ismaxidl  36908  mpobi123f  37030  mptbi12f  37034  disjressuc2  37258  qsdisjALTV  37485  parteq2  37645  lsatcmp  37873  lshpkrlem1  37980  trlval2  39034  cdlemg1cex  39459  cdlemm10N  39989  dicval  40047  lcmineqlem4  40897  fsuppind  41162  nnn1suc  41180  resubval  41240  unxpwdom3  41837  dgraalem  41887  dgraaub  41890  onsucf1lem  42019  frege104  42718  pm13.192  43169  2sbc6g  43174  2sbc5g  43175  pm14.122b  43182  equncomVD  43629  csbingVD  43645  csbsngVD  43654  csbxpgVD  43655  csbresgVD  43656  csbrngVD  43657  csbima12gALTVD  43658  csbunigVD  43659  csbfv12gALTVD  43660  relopabVD  43662  dvnprodlem1  44662  dvnprodlem2  44663  dvnprodlem3  44664  dvnprod  44665  fourierdlem42  44865  etransclem11  44961  etransclem12  44962  etransclem33  44983  nnfoctbdjlem  45171  hoimbl  45347  cfsetsnfsetf  45768  aiota0def  45804  euoreqb  45817  funressndmafv2rn  45931  funressnbrafv2  45952  dfatbrafv2b  45953  funbrafv2  45955  fnbrafv2b  45956  elsetpreimafvbi  46059  elsetpreimafveq  46065  imasetpreimafvbijlemfo  46073  fargshiftf1  46109  ichnreuop  46140  paireqne  46179  reupr  46190  uspgrsprf1  46525  uspgrsprfo  46526  lidldomn1  46823  nn0sumshdiglem2  47308  mof0  47504  eufsnlem  47507  isthincd2lem1  47647  setrec2lem2  47739