Theorem eqeq2 2747

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  eqeq2i  2748  eqtr3  2757  clelab  2880  alexeqg  3630  pm13.183  3645  elab6g  3648  eqeu  3689  moeq3  3695  mo2icl  3697  mob2  3698  euind  3707  reu6i  3711  reu2eqd  3719  reuind  3736  sbc2or  3774  sbc5ALT  3794  csbiebg  3906  eqif  4542  sneq  4611  reusngf  4650  rexreusng  4655  reuprg0  4678  preq1b  4822  preq12bg  4829  preqsn  4838  disji2  5103  disjprg  5115  dtruALT  5358  opth  5451  euotd  5488  solin  5588  ideqg  5831  resieq  5977  cnveqb  6185  cnveq0  6186  reu3op  6281  reuop  6282  iota5  6513  funopg  6569  fneq2  6629  foeq3  6787  tz6.12f  6901  funbrfv  6926  fnbrfvb  6928  fvelimab  6950  elrnrexdm  7078  funsndifnop  7140  fconst5  7197  eufnfv  7220  f1veqaeq  7248  fpropnf1  7259  nf1const  7296  isosolem  7339  f1opr  7461  mpoeq123  7477  ovmpt4g  7552  ov3  7568  ovg  7570  caovcang  7606  caovcan  7609  tfisi  7852  tfindsg  7854  findsg  7891  f1oweALT  7969  seqomlem2  8463  oawordeu  8565  omopth  8672  ereq2  8725  qsdisj  8806  eroveu  8824  2dom  9042  fundmen  9043  xpf1o  9151  nneneq  9218  pwfir  9325  cantnflem1  9701  brttrcl  9725  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  updjud  9946  alephfp  10120  dfac5  10141  cardcf  10264  cfeq0  10268  sornom  10289  fpwwe2cbv  10642  fpwwe2lem3  10645  ltsosr  11106  map2psrpr  11122  axpre-lttri  11177  subval  11471  divval  11896  nn0ind-raph  12691  fvf1tp  13804  uzrdgfni  13974  sqeqor  14232  nn0opth2  14288  hashrabsn1  14390  elprchashprn2  14412  hashbclem  14468  hashbc  14469  hash2prde  14486  hash2pwpr  14492  brfi1indALT  14526  wrdind  14738  wrd2ind  14739  reuccatpfxs1lem  14762  cshf1  14826  wrdl3s3  14979  relexpindlem  15080  sqrtval  15254  sqrmo  15268  reusq0  15479  summolem2  15730  prodmolem2  15949  divides  16272  dvdstr  16311  odd2np1lem  16357  ndvdssub  16426  bitsinv1  16459  eucalglt  16602  hashgcdeq  16807  ramcl2lem  17027  ramcl  17047  cshwrepswhash1  17120  imasaddfnlem  17540  fnhomeqhomf  17701  initoeu2lem1  18025  cat1lem  18107  posi  18327  sgrp2nmndlem3  18901  dfgrp2  18943  grpidinv  18979  dfgrp3lem  19019  orbsta  19294  symgfvne  19360  symgfix2  19395  odlem1  19514  gexlem1  19558  slwispgp  19590  sylow3lem6  19611  efgrelexlemb  19729  gsumval3lem2  19885  pgpfac1  20061  pgpfaclem2  20063  pgpfac  20065  ablfaclem1  20066  isdomn  20663  isdomn4  20674  domnlcanb  20678  domnrcanb  20680  obsip  21679  uvcval  21743  mvrval  21940  mhpval  22075  psdfval  22094  psdmvr  22105  coe1tmmul2  22211  coe1tmmul  22212  mat1comp  22376  mat1dimid  22410  scmateALT  22448  marrepval  22498  marepvval  22503  minmar1val  22584  gsummatr01  22595  t0sep  23260  t1sep2  23305  is2ndc  23382  kqt0lem  23672  isr0  23673  isufil2  23844  xmeteq0  24275  imasf1oxmet  24312  xrsxmet  24747  iccpnfcnv  24891  dyadmax  25549  dyadmbl  25551  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem1  25982  mdegle0  26032  fta1g  26125  ig1peu  26130  fta1  26266  aalioulem2  26291  taylthlem2  26332  efopn  26617  efrlim  26929  efrlimOLD  26930  musum  27151  mpodvdsmulf1o  27154  dvdsmulf1o  27156  dchrsum2  27229  sumdchr2  27231  gausslemma2dlem0i  27325  addsqnreup  27404  2sqreulem1  27407  2sqreultblem  27409  2sqreunnlem1  27410  2sqreunnltblem  27412  2sqreulem3  27414  sltres  27624  nosupprefixmo  27662  noinfprefixmo  27663  nosupcbv  27664  nosupno  27665  nosupfv  27668  noinfcbv  27679  noinfno  27680  noinffv  27683  elmade  27823  divsval  28132  noseqrdgfn  28229  axtgcgrid  28388  axtgbtwnid  28391  tglowdim1i  28426  islmib  28712  axcontlem12  28900  upgredgpr  29067  ushgredgedg  29154  ushgredgedgloop  29156  rusgrpropnb  29509  rgrx0ndm  29519  uspgr2wlkeq  29572  wlkson  29582  upgrwlkdvdelem  29664  spthonepeq  29680  iswwlksnon  29781  wlklnwwlkln2lem  29810  wwlksnredwwlkn  29823  wwlksnextprop  29840  wwlksnwwlksnon  29843  elwwlks2ons3  29883  rusgrnumwwlklem  29898  clwlkclwwlklem2a4  29924  clwwlkn  29953  clwwlkext2edg  29983  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwwlknon  30017  clwwlk0on0  30019  uhgr3cyclexlem  30108  1conngr  30121  frgr3vlem1  30200  3vfriswmgrlem  30204  frgrwopreglem3  30241  fusgreg2wsplem  30260  fusgreghash2wsp  30265  numclwlk1lem1  30296  numclwwlkovq  30301  numclwwlk2lem1  30303  frgrregord013  30322  friendshipgt3  30325  ex-opab  30359  isgrpoi  30425  grpoidinv2  30442  hvsubeq0  30995  hvaddcan  30997  hvsubadd  31004  normsub0  31063  omlsi  31331  pjoml  31363  nonbooli  31578  pj11  31641  lnopeq  31936  nmopun  31941  pjclem4a  32125  pj3lem1  32133  strlem4  32181  hstrlem4  32189  jplem1  32195  superpos  32281  ifeqeqx  32469  disji2f  32504  disjif2  32508  disjabrex  32509  disjabrexf  32510  disjxpin  32515  disjunsn  32521  ofpreima  32589  fgreu  32596  fcnvgreu  32597  sgnsub  32762  gsumhashmul  33001  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  domnlcanOLD  33220  ismxidl  33423  xrge0iifcnv  33910  esumpr2  34044  eulerpartlemgvv  34354  eulerpartlemgh  34356  eulerpartlemgs2  34358  plymulx0  34525  lpadmax  34660  lpadright  34662  bnj1321  35004  f1resfz0f1d  35082  subfacp1lem3  35150  pconncn  35192  cnpconn  35198  txpconn  35200  connpconn  35203  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3  35296  snmlflim  35300  iota5f  35687  rankeq1o  36135  nn0prpw  36287  bj-csbsnlem  36867  bj-elgab  36903  bj-restsnss  37047  bj-restsnss2  37048  bj-imdirco  37154  wl-isseteq  37469  wl-ax12v2cl  37470  fin2so  37577  poimirlem2  37592  poimirlem18  37608  poimirlem21  37611  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  mblfinlem2  37628  mbfresfi  37636  cnambfre  37638  ftc1anclem8  37670  fdc  37715  istotbnd  37739  isexid2  37825  isgrpda  37925  ismaxidl  38010  mpobi123f  38132  mptbi12f  38136  disjressuc2  38352  qsdisjALTV  38579  parteq2  38739  lsatcmp  38967  lshpkrlem1  39074  trlval2  40128  cdlemg1cex  40553  cdlemm10N  41083  dicval  41141  lcmineqlem4  41991  grpods  42153  unitscyglem2  42155  unitscyglem3  42156  unitscyglem4  42157  exfinfldd  42162  nnn1suc  42263  resubval  42357  fsuppind  42560  unxpwdom3  43066  dgraalem  43116  dgraaub  43119  onsucf1lem  43240  frege104  43938  pm13.192  44382  2sbc6g  44387  2sbc5g  44388  pm14.122b  44395  equncomVD  44840  csbingVD  44856  csbsngVD  44865  csbxpgVD  44866  csbresgVD  44867  csbrngVD  44868  csbima12gALTVD  44869  csbunigVD  44870  csbfv12gALTVD  44871  relopabVD  44873  dvnprodlem1  45923  dvnprodlem2  45924  dvnprodlem3  45925  dvnprod  45926  fourierdlem42  46126  etransclem11  46222  etransclem12  46223  etransclem33  46244  nnfoctbdjlem  46432  hoimbl  46608  cfsetsnfsetf  47035  aiota0def  47073  euoreqb  47086  funressndmafv2rn  47200  funressnbrafv2  47221  dfatbrafv2b  47222  funbrafv2  47224  fnbrafv2b  47225  elsetpreimafvbi  47353  elsetpreimafveq  47359  imasetpreimafvbijlemfo  47367  fargshiftf1  47403  ichnreuop  47434  paireqne  47473  reupr  47484  isuspgrim0  47855  upgrimpths  47870  clnbgrgrim  47895  grimedg  47896  isubgr3stgrlem4  47929  isubgr3stgrlem7  47932  uspgrsprf1  48070  uspgrsprfo  48071  lidldomn1  48154  nn0sumshdiglem2  48550  mof0  48764  eufsnlem  48767  oppcmndclem  48940  isthincd2lem1  49259  termcbasmo  49316  termcarweu  49361  arweuthinc  49362  arweutermc  49363  setrec2lem2  49506