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 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

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

This theorem is used by:  eqeq2i  2776  eqtr3  2785  clelab  2907  alexeqg  3607  pm13.183  3622  elab6g  3625  eqeu  3666  moeq3  3672  mo2icl  3674  mob2  3675  euind  3684  reu6i  3688  reu2eqd  3696  reuind  3713  sbc2or  3750  sbc5ALT  3770  csbiebg  3882  eqif  4526  sneq  4593  reusngf  4634  rexreusng  4639  reuprg0  4662  preq1b  4803  preq12bg  4810  preqsn  4819  disji2  5089  disjprg  5101  dtruALT  5353  opth  5448  euotd  5489  solin  5589  ideqg  5833  resieq  5985  reu3op  6301  reuop  6302  iota5  6528  funopg  6582  fneq2  6639  foeq3  6802  tz6.12f  6918  funbrfv  6941  fnbrfvb  6943  fvelimab  6965  elrnrexdm  7097  funsndifnop  7163  fconst5  7219  eufnfv  7242  f1veqaeq  7267  fpropnf1  7278  nf1const  7319  isosolem  7362  f1opr  7483  mpoeq123  7499  ovmpt4g  7574  ov3  7590  ovg  7592  caovcang  7629  caovcan  7632  tfisi  7877  tfindsg  7879  findsg  7916  f1oweALT  7991  seqomlem2  8472  oawordeu  8574  omopth  8682  ereq2  8737  qsdisj  8826  eroveu  8844  2dom  9069  fundmen  9070  xpf1o  9169  nneneq  9232  pwfir  9319  cantnflem1  9700  brttrcl  9724  ttrcltr  9727  ttrclss  9731  ttrclselem2  9737  setrec2lem2  9986  updjud  10025  alephfp  10197  dfac5  10217  cardcf  10339  cfeq0  10344  sornom  10365  fpwwe2cbv  10725  fpwwe2lem3  10728  ltsosr  11189  map2psrpr  11205  axpre-lttri  11260  subval  11558  divval  11986  nn0ind-raph  12809  f1resfz0f1d  13937  fvf1tp  13939  uzrdgfni  14111  sqeqor  14370  nn0opth2  14426  hashrabsn1  14528  elprchashprn2  14550  hashbclem  14607  hashbc  14608  hash2prde  14625  hash2pwpr  14631  brfi1indALT  14665  wrdind  14882  wrd2ind  14883  reuccatpfxs1lem  14906  cshf1  14972  wrdl3s3  15127  relexpindlem  15228  sgnsub  15271  sqrtval  15416  sqrmo  15430  reusq0  15644  summolem2  15894  prodmolem2  16114  divides  16436  dvdstr  16476  odd2np1lem  16522  ndvdssub  16591  bitsinv1  16624  eucalglt  16772  hashgcdeq  16979  ramcl2lem  17199  ramcl  17219  cshwrepswhash1  17292  imasaddfnlem  17712  fnhomeqhomf  17877  initoeu2lem1  18201  cat1lem  18283  posi  18503  sgrp2nmndlem3  19136  degenmgm2nfun  19151  dfgrp2  19185  grpidinv  19221  dfgrp3lem  19260  orbsta  19539  symgfvne  19607  symgfix2  19642  odlem1  19761  gexlem1  19805  slwispgp  19837  sylow3lem6  19858  efgrelexlemb  19976  gsumval3lem2  20132  pgpfac1  20308  pgpfaclem2  20310  pgpfac  20312  ablfaclem1  20313  isdomn  20969  isdomn4  20979  domnlcanb  20983  domnrcanb  20985  obsip  22039  uvcval  22103  mvrval  22301  mhpval  22472  psdfval  22491  psdmvr  22502  coe1tmmul2  22607  coe1tmmul  22608  mat1comp  22767  mat1dimid  22801  scmateALT  22839  marrepval  22889  marepvval  22894  minmar1val  22975  gsummatr01  22986  t0sep  23654  t1sep2  23699  is2ndc  23776  kqt0lem  24067  isr0  24068  isufil2  24239  xmeteq0  24669  imasf1oxmet  24706  xrsxmet  25141  iccpnfcnv  25277  dyadmax  25931  dyadmbl  25933  dvfsumle  26353  dvfsumabs  26355  dvfsumlem1  26358  mdegle0  26407  fta1g  26500  ig1peu  26505  plyn0mulidp  26614  fta1  26641  aalioulem2  26672  taylthlem2  26713  efopn  26998  efrlim  27309  musum  27530  mpodvdsmulf1o  27533  dvdsmulf1o  27535  dchrsum2  27607  sumdchr2  27609  gausslemma2dlem0i  27703  addsqnreup  27782  2sqreulem1  27785  2sqreultblem  27787  2sqreunnlem1  27788  2sqreunnltblem  27790  2sqreulem3  27792  ltsres  28031  nosupprefixmo  28069  noinfprefixmo  28070  nosupcbv  28071  nosupno  28072  nosupfv  28075  noinfcbv  28086  noinfno  28087  noinffv  28090  elmade  28255  divsval  28587  noseqrdgfn  28704  bdayn0sf1o  28768  bdayfinbndlem2  28866  axtgcgrid  28937  axtgbtwnid  28940  tglowdim1i  28976  islmib  29304  prlngmo2  29446  axcontlem12  29565  upgredgpr  29732  ushgredgedg  29822  ushgredgedgloop  29824  rusgrpropnb  30176  rgrx0ndm  30186  uspgr2wlkeq  30238  wlkson  30247  upgrwlkdvdelem  30334  spthonepeq  30350  iswwlksnon  30454  wlklnwwlkln2lem  30483  wwlksnredwwlkn  30496  wwlksnextprop  30513  wwlksnwwlksnon  30516  elwwlks2ons3  30556  rusgrnumwwlklem  30574  clwlkclwwlklem2a4  30600  clwwlkn  30629  clwwlkext2edg  30659  hashecclwwlkn1  30680  umgrhashecclwwlk  30681  clwwlknon  30693  clwwlk0on0  30695  uhgr3cyclexlem  30794  1conngr  30807  frgr3vlem1  30886  3vfriswmgrlem  30890  frgrwopreglem3  30927  fusgreg2wsplem  30946  fusgreghash2wsp  30951  numclwlk1lem1  30982  numclwwlkovq  30987  numclwwlk2lem1  30989  frgrregord013  31008  friendshipgt3  31011  ex-opab  31045  isgrpoi  31112  grpoidinv2  31129  hvsubeq0  31682  hvaddcan  31684  hvsubadd  31691  normsub0  31750  omlsi  32018  pjoml  32050  nonbooli  32265  pj11  32328  lnopeq  32623  nmopun  32628  pjclem4a  32812  pj3lem1  32820  strlem4  32868  hstrlem4  32876  jplem1  32882  superpos  32968  ifeqeqx  33192  disji2f  33225  disjif2  33229  disjabrex  33230  disjabrexf  33231  disjxpin  33236  disjunsn  33242  ofpreima  33313  fgreu  33319  fcnvgreu  33320  gsumhashmul  33681  elrgspnlem2  33857  elrgspnlem3  33858  elrgspnlem4  33859  ismxidl  34040  mplasclco  34201  mplmulmvr  34224  psrmonmul2  34236  esplyfval  34248  esplyfval0  34249  esplyfv  34255  esplyfval3  34257  esplyfvaln  34259  xrge0iifcnv  34618  esumpr2  34752  eulerpartlemgvv  35061  eulerpartlemgh  35063  eulerpartlemgs2  35065  lpadmax  35367  lpadright  35369  bnj1321  35710  subfacp1lem3  36068  pconncn  36110  cnpconn  36116  txpconn  36118  connpconn  36121  cvmlift3lem2  36206  cvmlift3lem4  36208  cvmlift3  36214  snmlflim  36218  mirimanoffr  36581  iota5f  36616  rankeq1o  37059  nn0prpw  37238  tr0elw  37399  tr0el  37400  dfttc4lem1  37443  elttcirr  37446  bj-csbsnlem  37942  bj-elgab  37979  bj-restsnss  38143  bj-restsnss2  38144  bj-imdirco  38251  wl-isseteq  38568  wl-ax12v2cl  38569  wl-dfcleq  38577  fin2so  38670  poimirlem2  38680  poimirlem18  38696  poimirlem21  38699  poimirlem25  38703  poimirlem26  38704  poimirlem27  38705  mblfinlem2  38716  mbfresfi  38724  cnambfre  38726  ftc1anclem8  38758  findcard4  38772  fdc  38819  istotbnd  38843  isexid2  38929  isgrpda  39029  ismaxidl  39114  mpobi123f  39234  mptbi12f  39238  disjressuc2  39483  qsdisjALTV  39771  parteq2  39950  lsatcmp  40200  lshpkrlem1  40307  trlval2  41360  cdlemg1cex  41785  cdlemm10N  42315  dicval  42373  lcmineqlem4  43222  grpods  43384  unitscyglem2  43386  unitscyglem3  43387  unitscyglem4  43388  exfinfldd  43393  nnn1suc  43471  resubval  43558  redivvald  43633  fsuppind  43758  unxpwdom3  44237  dgraalem  44287  dgraaub  44290  onsucf1lem  44411  frege104  45107  pm13.192  45534  2sbc6g  45539  2sbc5g  45540  pm14.122b  45546  equncomVD  45989  csbingVD  46005  csbsngVD  46014  csbxpgVD  46015  csbresgVD  46016  csbrngVD  46017  csbima12gALTVD  46018  csbunigVD  46019  csbfv12gALTVD  46020  relopabVD  46022  dvnprodlem1  47095  dvnprodlem2  47096  dvnprodlem3  47097  dvnprod  47098  fourierdlem42  47298  etransclem11  47394  etransclem12  47395  etransclem33  47416  nnfoctbdjlem  47604  hoimbl  47780  cfsetsnfsetf  48267  aiota0def  48305  euoreqb  48319  funressndmafv2rn  48432  funressnbrafv2  48453  dfatbrafv2b  48454  funbrafv2  48456  fnbrafv2b  48457  elsetpreimafvbi  48612  elsetpreimafveq  48618  imasetpreimafvbijlemfo  48626  fargshiftf1  48662  ichnreuop  48693  paireqne  48732  reupr  48743  isuspgrim0  49131  upgrimpths  49146  clnbgrgrim  49171  grimedg  49172  isubgr3stgrlem4  49206  isubgr3stgrlem7  49209  gpgedg2ov  49303  gpgedg2iv  49304  pgnbgreunbgrlem1  49350  pgnbgreunbgrlem2lem3  49353  pgnbgreunbgrlem4  49356  pgnbgreunbgr  49362  uspgrsprf1  49384  uspgrsprfo  49385  lidldomn1  49467  nn0sumshdiglem2  49873  mof0  50088  eufsnlem  50091  oppcmndclem  50270  isthincd2lem1  50699  termcbasmo  50757  termcarweu  50802  arweuthinc  50803  arweutermc  50804