Theorem eqeq2 2741

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 2740	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqeq2i  2742  eqtr3  2751  clelab  2873  alexeqg  3614  pm13.183  3629  elab6g  3632  eqeu  3674  moeq3  3680  mo2icl  3682  mob2  3683  euind  3692  reu6i  3696  reu2eqd  3704  reuind  3721  sbc2or  3759  sbc5ALT  3779  csbiebg  3891  eqif  4526  sneq  4595  reusngf  4634  rexreusng  4639  reuprg0  4662  preq1b  4806  preq12bg  4813  preqsn  4822  disji2  5086  disjprg  5098  dtruALT  5338  opth  5431  euotd  5468  solin  5566  ideqg  5805  resieq  5950  cnveqb  6157  cnveq0  6158  reu3op  6253  reuop  6254  iota5  6482  funopg  6534  fneq2  6592  foeq3  6752  tz6.12f  6866  funbrfv  6891  fnbrfvb  6893  fvelimab  6915  elrnrexdm  7043  funsndifnop  7105  fconst5  7162  eufnfv  7185  f1veqaeq  7213  fpropnf1  7224  nf1const  7261  isosolem  7304  f1opr  7425  mpoeq123  7441  ovmpt4g  7516  ov3  7532  ovg  7534  caovcang  7570  caovcan  7573  tfisi  7815  tfindsg  7817  findsg  7853  f1oweALT  7930  seqomlem2  8396  oawordeu  8496  omopth  8603  ereq2  8656  qsdisj  8744  eroveu  8762  2dom  8978  fundmen  8979  xpf1o  9080  nneneq  9147  pwfir  9242  cantnflem1  9618  brttrcl  9642  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  updjud  9863  alephfp  10037  dfac5  10058  cardcf  10181  cfeq0  10185  sornom  10206  fpwwe2cbv  10559  fpwwe2lem3  10562  ltsosr  11023  map2psrpr  11039  axpre-lttri  11094  subval  11388  divval  11815  nn0ind-raph  12610  fvf1tp  13727  uzrdgfni  13899  sqeqor  14157  nn0opth2  14213  hashrabsn1  14315  elprchashprn2  14337  hashbclem  14393  hashbc  14394  hash2prde  14411  hash2pwpr  14417  brfi1indALT  14451  wrdind  14663  wrd2ind  14664  reuccatpfxs1lem  14687  cshf1  14751  wrdl3s3  14904  relexpindlem  15005  sqrtval  15179  sqrmo  15193  reusq0  15407  summolem2  15658  prodmolem2  15877  divides  16200  dvdstr  16240  odd2np1lem  16286  ndvdssub  16355  bitsinv1  16388  eucalglt  16531  hashgcdeq  16736  ramcl2lem  16956  ramcl  16976  cshwrepswhash1  17049  imasaddfnlem  17467  fnhomeqhomf  17632  initoeu2lem1  17956  cat1lem  18038  posi  18258  sgrp2nmndlem3  18834  dfgrp2  18876  grpidinv  18912  dfgrp3lem  18952  orbsta  19227  symgfvne  19295  symgfix2  19330  odlem1  19449  gexlem1  19493  slwispgp  19525  sylow3lem6  19546  efgrelexlemb  19664  gsumval3lem2  19820  pgpfac1  19996  pgpfaclem2  19998  pgpfac  20000  ablfaclem1  20001  isdomn  20625  isdomn4  20636  domnlcanb  20640  domnrcanb  20642  obsip  21663  uvcval  21727  mvrval  21924  mhpval  22059  psdfval  22078  psdmvr  22089  coe1tmmul2  22195  coe1tmmul  22196  mat1comp  22360  mat1dimid  22394  scmateALT  22432  marrepval  22482  marepvval  22487  minmar1val  22568  gsummatr01  22579  t0sep  23244  t1sep2  23289  is2ndc  23366  kqt0lem  23656  isr0  23657  isufil2  23828  xmeteq0  24259  imasf1oxmet  24296  xrsxmet  24731  iccpnfcnv  24875  dyadmax  25532  dyadmbl  25534  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem1  25965  mdegle0  26015  fta1g  26108  ig1peu  26113  fta1  26249  aalioulem2  26274  taylthlem2  26315  efopn  26600  efrlim  26912  efrlimOLD  26913  musum  27134  mpodvdsmulf1o  27137  dvdsmulf1o  27139  dchrsum2  27212  sumdchr2  27214  gausslemma2dlem0i  27308  addsqnreup  27387  2sqreulem1  27390  2sqreultblem  27392  2sqreunnlem1  27393  2sqreunnltblem  27395  2sqreulem3  27397  sltres  27607  nosupprefixmo  27645  noinfprefixmo  27646  nosupcbv  27647  nosupno  27648  nosupfv  27651  noinfcbv  27662  noinfno  27663  noinffv  27666  elmade  27816  divsval  28132  noseqrdgfn  28240  bdayn0sf1o  28299  axtgcgrid  28443  axtgbtwnid  28446  tglowdim1i  28481  islmib  28767  axcontlem12  28955  upgredgpr  29122  ushgredgedg  29209  ushgredgedgloop  29211  rusgrpropnb  29564  rgrx0ndm  29574  uspgr2wlkeq  29626  wlkson  29635  upgrwlkdvdelem  29716  spthonepeq  29732  iswwlksnon  29833  wlklnwwlkln2lem  29862  wwlksnredwwlkn  29875  wwlksnextprop  29892  wwlksnwwlksnon  29895  elwwlks2ons3  29935  rusgrnumwwlklem  29950  clwlkclwwlklem2a4  29976  clwwlkn  30005  clwwlkext2edg  30035  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  clwwlknon  30069  clwwlk0on0  30071  uhgr3cyclexlem  30160  1conngr  30173  frgr3vlem1  30252  3vfriswmgrlem  30256  frgrwopreglem3  30293  fusgreg2wsplem  30312  fusgreghash2wsp  30317  numclwlk1lem1  30348  numclwwlkovq  30353  numclwwlk2lem1  30355  frgrregord013  30374  friendshipgt3  30377  ex-opab  30411  isgrpoi  30477  grpoidinv2  30494  hvsubeq0  31047  hvaddcan  31049  hvsubadd  31056  normsub0  31115  omlsi  31383  pjoml  31415  nonbooli  31630  pj11  31693  lnopeq  31988  nmopun  31993  pjclem4a  32177  pj3lem1  32185  strlem4  32233  hstrlem4  32241  jplem1  32247  superpos  32333  ifeqeqx  32521  disji2f  32556  disjif2  32560  disjabrex  32561  disjabrexf  32562  disjxpin  32567  disjunsn  32573  ofpreima  32639  fgreu  32646  fcnvgreu  32647  sgnsub  32812  gsumhashmul  33044  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  domnlcanOLD  33246  ismxidl  33426  xrge0iifcnv  33916  esumpr2  34050  eulerpartlemgvv  34360  eulerpartlemgh  34362  eulerpartlemgs2  34364  plymulx0  34531  lpadmax  34666  lpadright  34668  bnj1321  35010  f1resfz0f1d  35094  subfacp1lem3  35162  pconncn  35204  cnpconn  35210  txpconn  35212  connpconn  35215  cvmlift3lem2  35300  cvmlift3lem4  35302  cvmlift3  35308  snmlflim  35312  iota5f  35704  rankeq1o  36152  nn0prpw  36304  bj-csbsnlem  36884  bj-elgab  36920  bj-restsnss  37064  bj-restsnss2  37065  bj-imdirco  37171  wl-isseteq  37486  wl-ax12v2cl  37487  fin2so  37594  poimirlem2  37609  poimirlem18  37625  poimirlem21  37628  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  mblfinlem2  37645  mbfresfi  37653  cnambfre  37655  ftc1anclem8  37687  fdc  37732  istotbnd  37756  isexid2  37842  isgrpda  37942  ismaxidl  38027  mpobi123f  38149  mptbi12f  38153  disjressuc2  38367  qsdisjALTV  38599  parteq2  38760  lsatcmp  38989  lshpkrlem1  39096  trlval2  40150  cdlemg1cex  40575  cdlemm10N  41105  dicval  41163  lcmineqlem4  42013  grpods  42175  unitscyglem2  42177  unitscyglem3  42178  unitscyglem4  42179  exfinfldd  42184  nnn1suc  42247  resubval  42348  redivvald  42423  fsuppind  42571  unxpwdom3  43077  dgraalem  43127  dgraaub  43130  onsucf1lem  43251  frege104  43949  pm13.192  44392  2sbc6g  44397  2sbc5g  44398  pm14.122b  44405  equncomVD  44850  csbingVD  44866  csbsngVD  44875  csbxpgVD  44876  csbresgVD  44877  csbrngVD  44878  csbima12gALTVD  44879  csbunigVD  44880  csbfv12gALTVD  44881  relopabVD  44883  dvnprodlem1  45937  dvnprodlem2  45938  dvnprodlem3  45939  dvnprod  45940  fourierdlem42  46140  etransclem11  46236  etransclem12  46237  etransclem33  46258  nnfoctbdjlem  46446  hoimbl  46622  cfsetsnfsetf  47052  aiota0def  47090  euoreqb  47103  funressndmafv2rn  47217  funressnbrafv2  47238  dfatbrafv2b  47239  funbrafv2  47241  fnbrafv2b  47242  elsetpreimafvbi  47385  elsetpreimafveq  47391  imasetpreimafvbijlemfo  47399  fargshiftf1  47435  ichnreuop  47466  paireqne  47505  reupr  47516  isuspgrim0  47887  upgrimpths  47902  clnbgrgrim  47927  grimedg  47928  isubgr3stgrlem4  47961  isubgr3stgrlem7  47964  gpgedg2ov  48050  gpgedg2iv  48051  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem2lem3  48099  pgnbgreunbgrlem4  48102  pgnbgreunbgr  48108  uspgrsprf1  48128  uspgrsprfo  48129  lidldomn1  48212  nn0sumshdiglem2  48604  mof0  48819  eufsnlem  48822  oppcmndclem  48999  isthincd2lem1  49407  termcbasmo  49465  termcarweu  49510  arweuthinc  49511  arweutermc  49512  setrec2lem2  49676