Theorem eqeq2 2749

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqeq2i  2750  eqtr3  2759  clelab  2881  alexeqg  3607  pm13.183  3622  elab6g  3625  eqeu  3666  moeq3  3672  mo2icl  3674  mob2  3675  euind  3684  reu6i  3688  reu2eqd  3696  reuind  3713  sbc2or  3751  sbc5ALT  3771  csbiebg  3883  eqif  4523  sneq  4592  reusngf  4633  rexreusng  4638  reuprg0  4661  preq1b  4804  preq12bg  4811  preqsn  4820  disji2  5084  disjprg  5096  dtruALT  5335  opth  5432  euotd  5469  solin  5567  ideqg  5808  resieq  5957  cnveqb  6162  cnveq0  6163  reu3op  6258  reuop  6259  iota5  6483  funopg  6534  fneq2  6592  foeq3  6752  tz6.12f  6867  funbrfv  6890  fnbrfvb  6892  fvelimab  6914  elrnrexdm  7043  funsndifnop  7106  fconst5  7162  eufnfv  7185  f1veqaeq  7212  fpropnf1  7223  nf1const  7260  isosolem  7303  f1opr  7424  mpoeq123  7440  ovmpt4g  7515  ov3  7531  ovg  7533  caovcang  7569  caovcan  7572  tfisi  7811  tfindsg  7813  findsg  7849  f1oweALT  7926  seqomlem2  8392  oawordeu  8492  omopth  8600  ereq2  8654  qsdisj  8743  eroveu  8761  2dom  8979  fundmen  8980  xpf1o  9079  nneneq  9142  pwfir  9229  cantnflem1  9610  brttrcl  9634  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  updjud  9858  alephfp  10030  dfac5  10051  cardcf  10174  cfeq0  10178  sornom  10199  fpwwe2cbv  10553  fpwwe2lem3  10556  ltsosr  11017  map2psrpr  11033  axpre-lttri  11088  subval  11383  divval  11810  nn0ind-raph  12604  fvf1tp  13721  uzrdgfni  13893  sqeqor  14151  nn0opth2  14207  hashrabsn1  14309  elprchashprn2  14331  hashbclem  14387  hashbc  14388  hash2prde  14405  hash2pwpr  14411  brfi1indALT  14445  wrdind  14657  wrd2ind  14658  reuccatpfxs1lem  14681  cshf1  14745  wrdl3s3  14897  relexpindlem  14998  sqrtval  15172  sqrmo  15186  reusq0  15400  summolem2  15651  prodmolem2  15870  divides  16193  dvdstr  16233  odd2np1lem  16279  ndvdssub  16348  bitsinv1  16381  eucalglt  16524  hashgcdeq  16729  ramcl2lem  16949  ramcl  16969  cshwrepswhash1  17042  imasaddfnlem  17461  fnhomeqhomf  17626  initoeu2lem1  17950  cat1lem  18032  posi  18252  sgrp2nmndlem3  18862  dfgrp2  18904  grpidinv  18940  dfgrp3lem  18980  orbsta  19254  symgfvne  19322  symgfix2  19357  odlem1  19476  gexlem1  19520  slwispgp  19552  sylow3lem6  19573  efgrelexlemb  19691  gsumval3lem2  19847  pgpfac1  20023  pgpfaclem2  20025  pgpfac  20027  ablfaclem1  20028  isdomn  20650  isdomn4  20661  domnlcanb  20665  domnrcanb  20667  obsip  21688  uvcval  21752  mvrval  21949  mhpval  22094  psdfval  22113  psdmvr  22124  coe1tmmul2  22230  coe1tmmul  22231  mat1comp  22396  mat1dimid  22430  scmateALT  22468  marrepval  22518  marepvval  22523  minmar1val  22604  gsummatr01  22615  t0sep  23280  t1sep2  23325  is2ndc  23402  kqt0lem  23692  isr0  23693  isufil2  23864  xmeteq0  24294  imasf1oxmet  24331  xrsxmet  24766  iccpnfcnv  24910  dyadmax  25567  dyadmbl  25569  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem1  26000  mdegle0  26050  fta1g  26143  ig1peu  26148  fta1  26284  aalioulem2  26309  taylthlem2  26350  efopn  26635  efrlim  26947  efrlimOLD  26948  musum  27169  mpodvdsmulf1o  27172  dvdsmulf1o  27174  dchrsum2  27247  sumdchr2  27249  gausslemma2dlem0i  27343  addsqnreup  27422  2sqreulem1  27425  2sqreultblem  27427  2sqreunnlem1  27428  2sqreunnltblem  27430  2sqreulem3  27432  ltsres  27642  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupno  27683  nosupfv  27686  noinfcbv  27697  noinfno  27698  noinffv  27701  elmade  27865  divsval  28197  noseqrdgfn  28314  bdayn0sf1o  28378  bdayfinbndlem2  28476  axtgcgrid  28547  axtgbtwnid  28550  tglowdim1i  28585  islmib  28871  axcontlem12  29060  upgredgpr  29227  ushgredgedg  29314  ushgredgedgloop  29316  rusgrpropnb  29669  rgrx0ndm  29679  uspgr2wlkeq  29731  wlkson  29740  upgrwlkdvdelem  29821  spthonepeq  29837  iswwlksnon  29938  wlklnwwlkln2lem  29967  wwlksnredwwlkn  29980  wwlksnextprop  29997  wwlksnwwlksnon  30000  elwwlks2ons3  30040  rusgrnumwwlklem  30058  clwlkclwwlklem2a4  30084  clwwlkn  30113  clwwlkext2edg  30143  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwwlknon  30177  clwwlk0on0  30179  uhgr3cyclexlem  30268  1conngr  30281  frgr3vlem1  30360  3vfriswmgrlem  30364  frgrwopreglem3  30401  fusgreg2wsplem  30420  fusgreghash2wsp  30425  numclwlk1lem1  30456  numclwwlkovq  30461  numclwwlk2lem1  30463  frgrregord013  30482  friendshipgt3  30485  ex-opab  30519  isgrpoi  30586  grpoidinv2  30603  hvsubeq0  31156  hvaddcan  31158  hvsubadd  31165  normsub0  31224  omlsi  31492  pjoml  31524  nonbooli  31739  pj11  31802  lnopeq  32097  nmopun  32102  pjclem4a  32286  pj3lem1  32294  strlem4  32342  hstrlem4  32350  jplem1  32356  superpos  32442  ifeqeqx  32629  disji2f  32664  disjif2  32668  disjabrex  32669  disjabrexf  32670  disjxpin  32675  disjunsn  32681  ofpreima  32755  fgreu  32761  fcnvgreu  32762  sgnsub  32929  gsumhashmul  33161  elrgspnlem2  33337  elrgspnlem3  33338  elrgspnlem4  33339  domnlcanOLD  33374  ismxidl  33555  mplmulmvr  33716  psrmonmul2  33728  esplyfval  33740  esplyfval0  33741  esplyfv  33747  esplyfval3  33749  esplyfvaln  33751  xrge0iifcnv  34111  esumpr2  34245  eulerpartlemgvv  34554  eulerpartlemgh  34556  eulerpartlemgs2  34558  plymulx0  34725  lpadmax  34860  lpadright  34862  bnj1321  35203  f1resfz0f1d  35330  subfacp1lem3  35398  pconncn  35440  cnpconn  35446  txpconn  35448  connpconn  35451  cvmlift3lem2  35536  cvmlift3lem4  35538  cvmlift3  35544  snmlflim  35548  iota5f  35940  rankeq1o  36387  nn0prpw  36539  bj-csbsnlem  37151  bj-elgab  37187  bj-restsnss  37336  bj-restsnss2  37337  bj-imdirco  37445  wl-isseteq  37760  wl-ax12v2cl  37761  fin2so  37858  poimirlem2  37873  poimirlem18  37889  poimirlem21  37892  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  mblfinlem2  37909  mbfresfi  37917  cnambfre  37919  ftc1anclem8  37951  fdc  37996  istotbnd  38020  isexid2  38106  isgrpda  38206  ismaxidl  38291  mpobi123f  38413  mptbi12f  38417  disjressuc2  38662  qsdisjALTV  38950  parteq2  39129  lsatcmp  39379  lshpkrlem1  39486  trlval2  40539  cdlemg1cex  40964  cdlemm10N  41494  dicval  41552  lcmineqlem4  42402  grpods  42564  unitscyglem2  42566  unitscyglem3  42567  unitscyglem4  42568  exfinfldd  42573  nnn1suc  42636  resubval  42737  redivvald  42812  fsuppind  42948  unxpwdom3  43452  dgraalem  43502  dgraaub  43505  onsucf1lem  43626  frege104  44323  pm13.192  44766  2sbc6g  44771  2sbc5g  44772  pm14.122b  44779  equncomVD  45223  csbingVD  45239  csbsngVD  45248  csbxpgVD  45249  csbresgVD  45250  csbrngVD  45251  csbima12gALTVD  45252  csbunigVD  45253  csbfv12gALTVD  45254  relopabVD  45256  dvnprodlem1  46304  dvnprodlem2  46305  dvnprodlem3  46306  dvnprod  46307  fourierdlem42  46507  etransclem11  46603  etransclem12  46604  etransclem33  46625  nnfoctbdjlem  46813  hoimbl  46989  cfsetsnfsetf  47418  aiota0def  47456  euoreqb  47469  funressndmafv2rn  47583  funressnbrafv2  47604  dfatbrafv2b  47605  funbrafv2  47607  fnbrafv2b  47608  elsetpreimafvbi  47751  elsetpreimafveq  47757  imasetpreimafvbijlemfo  47765  fargshiftf1  47801  ichnreuop  47832  paireqne  47871  reupr  47882  isuspgrim0  48254  upgrimpths  48269  clnbgrgrim  48294  grimedg  48295  isubgr3stgrlem4  48329  isubgr3stgrlem7  48332  gpgedg2ov  48426  gpgedg2iv  48427  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem2lem3  48476  pgnbgreunbgrlem4  48479  pgnbgreunbgr  48485  uspgrsprf1  48507  uspgrsprfo  48508  lidldomn1  48591  nn0sumshdiglem2  48982  mof0  49197  eufsnlem  49200  oppcmndclem  49376  isthincd2lem1  49784  termcbasmo  49842  termcarweu  49887  arweuthinc  49888  arweutermc  49889  setrec2lem2  50053