Theorem eqeq2 2775

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq2d 2774	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  eqeq2i  2776  eqtr3  2785  clelab  2908  alexeqg  3608  pm13.183  3623  elab6g  3626  eqeu  3667  moeq3  3673  mo2icl  3675  mob2  3676  euind  3685  reu6i  3689  reu2eqd  3697  reuind  3714  sbc2or  3751  sbc5ALT  3771  csbiebg  3883  eqif  4527  sneq  4594  reusngf  4636  rexreusng  4641  reuprg0  4664  preq1b  4806  preq12bg  4813  preqsn  4822  disji2  5092  disjprg  5104  dtruALT  5357  opth  5452  euotd  5493  solin  5593  ideqg  5839  resieq  5997  reu3op  6321  reuop  6322  iota5  6548  funopg  6602  fneq2  6661  foeq3  6824  tz6.12f  6941  funbrfv  6964  fnbrfvb  6966  fvelimab  6988  elrnrexdm  7121  funsndifnop  7187  fconst5  7243  eufnfv  7266  f1veqaeq  7291  fpropnf1  7302  nf1const  7343  isosolem  7386  f1opr  7507  mpoeq123  7523  ovmpt4g  7599  ov3  7615  ovg  7617  caovcang  7654  caovcan  7657  tfisi  7904  tfindsg  7906  findsg  7943  f1oweALT  8018  seqomlem2  8499  oawordeu  8601  omopth  8709  ereq2  8764  qsdisj  8853  eroveu  8871  2dom  9096  fundmen  9097  xpf1o  9196  nneneq  9259  pwfir  9346  cantnflem1  9727  brttrcl  9751  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  setrec2lem2  10013  updjud  10052  alephfp  10226  dfac5  10246  cardcf  10368  cfeq0  10373  sornom  10394  fpwwe2cbv  10754  fpwwe2lem3  10757  ltsosr  11218  map2psrpr  11234  axpre-lttri  11289  subval  11587  divval  12016  nn0ind-raph  12839  f1resfz0f1d  13967  fvf1tp  13969  uzrdgfni  14141  sqeqor  14401  nn0opth2  14457  hashrabsn1  14559  elprchashprn2  14581  hashbclem  14638  hashbc  14639  hash2prde  14656  hash2pwpr  14662  brfi1indALT  14696  wrdind  14913  wrd2ind  14914  reuccatpfxs1lem  14937  cshf1  15003  wrdl3s3  15158  relexpindlem  15259  sgnsub  15302  sqrtval  15447  sqrmo  15461  reusq0  15676  summolem2  15926  prodmolem2  16146  divides  16468  dvdstr  16508  odd2np1lem  16554  ndvdssub  16623  bitsinv1  16656  eucalglt  16804  hashgcdeq  17011  ramcl2lem  17231  ramcl  17251  cshwrepswhash1  17324  imasaddfnlem  17750  fnhomeqhomf  17915  initoeu2lem1  18239  cat1lem  18321  posi  18541  sgrp2nmndlem3  19174  degenmgm2nfun  19189  dfgrp2  19223  grpidinv  19259  dfgrp3lem  19298  orbsta  19578  symgfvne  19646  symgfix2  19681  odlem1  19800  gexlem1  19844  slwispgp  19876  sylow3lem6  19897  efgrelexlemb  20015  gsumval3lem2  20171  pgpfac1  20347  pgpfaclem2  20349  pgpfac  20351  ablfaclem1  20352  isdomn  21008  isdomn4  21018  domnlcanb  21022  domnrcanb  21024  obsip  22082  uvcval  22146  mvrval  22344  mhpval  22515  psdfval  22534  psdmvr  22545  coe1tmmul2  22650  coe1tmmul  22651  mat1comp  22810  mat1dimid  22844  scmateALT  22882  marrepval  22932  marepvval  22937  minmar1val  23018  gsummatr01  23029  t0sep  23697  t1sep2  23742  is2ndc  23819  kqt0lem  24110  isr0  24111  isufil2  24282  xmeteq0  24712  imasf1oxmet  24749  xrsxmet  25184  iccpnfcnv  25320  dyadmax  25974  dyadmbl  25976  dvfsumle  26396  dvfsumabs  26398  dvfsumlem1  26401  mdegle0  26450  fta1g  26543  ig1peu  26548  plyn0mulidp  26657  fta1  26684  aalioulem2  26717  taylthlem2  26758  efopn  27043  efrlim  27354  musum  27575  mpodvdsmulf1o  27578  dvdsmulf1o  27580  dchrsum2  27652  sumdchr2  27654  gausslemma2dlem0i  27748  addsqnreup  27827  2sqreulem1  27830  2sqreultblem  27832  2sqreunnlem1  27833  2sqreunnltblem  27835  2sqreulem3  27837  ltsres  28076  nosupprefixmo  28114  noinfprefixmo  28115  nosupcbv  28116  nosupno  28117  nosupfv  28120  noinfcbv  28131  noinfno  28132  noinffv  28135  elmade  28300  divsval  28632  noseqrdgfn  28749  bdayn0sf1o  28813  bdayfinbndlem2  28911  axtgcgrid  28982  axtgbtwnid  28985  tglowdim1i  29021  islmib  29349  prlngmo2  29491  axcontlem12  29610  upgredgpr  29777  ushgredgedg  29867  ushgredgedgloop  29869  rusgrpropnb  30221  rgrx0ndm  30231  uspgr2wlkeq  30283  wlkson  30292  upgrwlkdvdelem  30379  spthonepeq  30395  iswwlksnon  30499  wlklnwwlkln2lem  30528  wwlksnredwwlkn  30541  wwlksnextprop  30558  wwlksnwwlksnon  30561  elwwlks2ons3  30601  rusgrnumwwlklem  30619  clwlkclwwlklem2a4  30645  clwwlkn  30674  clwwlkext2edg  30704  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  clwwlknon  30738  clwwlk0on0  30740  uhgr3cyclexlem  30839  1conngr  30852  frgr3vlem1  30931  3vfriswmgrlem  30935  frgrwopreglem3  30972  fusgreg2wsplem  30991  fusgreghash2wsp  30996  numclwlk1lem1  31027  numclwwlkovq  31032  numclwwlk2lem1  31034  frgrregord013  31053  friendshipgt3  31056  ex-opab  31090  isgrpoi  31157  grpoidinv2  31174  hvsubeq0  31727  hvaddcan  31729  hvsubadd  31736  normsub0  31795  omlsi  32063  pjoml  32095  nonbooli  32310  pj11  32373  lnopeq  32668  nmopun  32673  pjclem4a  32857  pj3lem1  32865  strlem4  32913  hstrlem4  32921  jplem1  32927  superpos  33013  ifeqeqx  33236  disji2f  33269  disjif2  33273  disjabrex  33274  disjabrexf  33275  disjxpin  33280  disjunsn  33286  ofpreima  33357  fgreu  33363  fcnvgreu  33364  gsumhashmul  33727  elrgspnlem2  33903  elrgspnlem3  33904  elrgspnlem4  33905  ismxidl  34091  mplasclco  34259  mplmulmvr  34282  psrmonmul2  34294  esplyfval  34306  esplyfval0  34307  esplyfv  34313  esplyfval3  34315  esplyfvaln  34317  xrge0iifcnv  34676  esumpr2  34810  eulerpartlemgvv  35119  eulerpartlemgh  35121  eulerpartlemgs2  35123  lpadmax  35425  lpadright  35427  bnj1321  35768  subfacp1lem3  36155  pconncn  36197  cnpconn  36203  txpconn  36205  connpconn  36208  cvmlift3lem2  36293  cvmlift3lem4  36295  cvmlift3  36301  snmlflim  36305  mirimanoffr  36668  elpssmo  36673  iota5f  36704  rankeq1o  37147  nn0prpw  37326  tr0elw  37487  tr0el  37488  dfttc4lem1  37531  elttcirr  37534  bj-csbsnlem  38030  bj-elgab  38067  bj-restsnss  38274  bj-restsnss2  38275  bj-imdirco  38379  wl-isseteq  38696  wl-ax12v2cl  38697  wl-dfcleq  38705  fin2so  38798  poimirlem2  38808  poimirlem18  38824  poimirlem21  38827  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  mblfinlem2  38844  mbfresfi  38852  cnambfre  38854  ftc1anclem8  38886  findcard4  38900  fdc  38945  istotbnd  38969  isexid2  39055  isgrpda  39155  ismaxidl  39240  mpobi123f  39360  mptbi12f  39364  disjressuc2  39609  qsdisjALTV  39897  parteq2  40076  lsatcmp  40326  lshpkrlem1  40433  trlval2  41486  cdlemg1cex  41911  cdlemm10N  42441  dicval  42499  lcmineqlem4  43348  grpods  43510  unitscyglem2  43512  unitscyglem3  43513  unitscyglem4  43514  exfinfldd  43519  nnn1suc  43597  resubval  43684  redivvald  43759  fsuppind  43884  unxpwdom3  44363  dgraalem  44412  dgraaub  44415  onsucf1lem  44532  frege104  45228  pm13.192  45655  2sbc6g  45660  2sbc5g  45661  pm14.122b  45667  equncomVD  46110  csbingVD  46126  csbsngVD  46135  csbxpgVD  46136  csbresgVD  46137  csbrngVD  46138  csbima12gALTVD  46139  csbunigVD  46140  csbfv12gALTVD  46141  relopabVD  46143  dvnprodlem1  47229  dvnprodlem2  47230  dvnprodlem3  47231  dvnprod  47232  fourierdlem42  47432  etransclem11  47528  etransclem12  47529  etransclem33  47550  nnfoctbdjlem  47738  hoimbl  47914  cfsetsnfsetf  48401  aiota0def  48439  euoreqb  48453  funressndmafv2rn  48566  funressnbrafv2  48587  dfatbrafv2b  48588  funbrafv2  48590  fnbrafv2b  48591  elsetpreimafvbi  48746  elsetpreimafveq  48752  imasetpreimafvbijlemfo  48760  fargshiftf1  48796  ichnreuop  48827  paireqne  48866  reupr  48877  isuspgrim0  49265  upgrimpths  49280  clnbgrgrim  49305  grimedg  49306  isubgr3stgrlem4  49340  isubgr3stgrlem7  49343  gpgedg2ov  49437  gpgedg2iv  49438  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2lem3  49487  pgnbgreunbgrlem4  49490  pgnbgreunbgr  49496  uspgrsprf1  49518  uspgrsprfo  49519  lidldomn1  49601  nn0sumshdiglem2  50065  mof0  50280  eufsnlem  50283  oppcmndclem  50462  isthincd2lem1  50891  termcbasmo  50949  termcarweu  50994  arweuthinc  50995  arweutermc  50996