Theorem eqeq2 2750

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  eqeq2i  2751  eqeq12OLD  2757  eqtr3  2764  clelab  2883  alexeqg  3581  pm13.183  3597  elab6g  3600  eqeu  3641  moeq3  3647  mo2icl  3649  mob2  3650  euind  3659  reu6i  3663  reu2eqd  3671  reuind  3688  sbc2or  3725  sbc5ALT  3745  csbiebg  3865  eqif  4500  sneq  4571  reusngf  4608  rexreusng  4615  reuprg0  4638  preq1b  4777  preq12bg  4784  preqsn  4792  disji2  5056  disjprgw  5069  disjprg  5070  dtruALT  5311  opth  5391  euotd  5427  solin  5528  ideqg  5760  resieq  5902  cnveqb  6099  cnveq0  6100  reu3op  6195  reuop  6196  iota5  6416  funopg  6468  fneq2  6525  foeq3  6686  tz6.12f  6798  funbrfv  6820  fnbrfvb  6822  fvelimab  6841  elrnrexdm  6965  funsndifnop  7023  fconst5  7081  eufnfv  7105  f1veqaeq  7130  fpropnf1  7140  nf1const  7176  isosolem  7218  f1opr  7331  mpoeq123  7347  ovmpt4g  7420  ov3  7435  ovg  7437  caovcang  7473  caovcan  7476  tfisi  7705  tfindsg  7707  findsg  7746  f1oweALT  7815  seqomlem2  8282  oawordeu  8386  omopth  8492  ereq2  8506  qsdisj  8583  eroveu  8601  2dom  8820  fundmen  8821  xpf1o  8926  pwfir  8959  nneneq  8992  nneneqOLD  9004  cantnflem1  9447  brttrcl  9471  ttrcltr  9474  ttrclss  9478  ttrclselem2  9484  updjud  9692  alephfp  9864  dfac5  9884  cardcf  10008  cfeq0  10012  sornom  10033  fpwwe2cbv  10386  fpwwe2lem3  10389  ltsosr  10850  map2psrpr  10866  axpre-lttri  10921  subval  11212  divval  11635  nn0ind-raph  12420  uzrdgfni  13678  sqeqor  13932  nn0opth2  13986  hashrabsn1  14089  elprchashprn2  14111  hashbclem  14164  hashbc  14165  hash2prde  14184  hash2pwpr  14190  brfi1indALT  14214  wrdind  14435  wrd2ind  14436  reuccatpfxs1lem  14459  cshf1  14523  wrdl3s3  14677  relexpindlem  14774  sqrtval  14948  sqrmo  14963  reusq0  15174  summolem2  15428  prodmolem2  15645  divides  15965  dvdstr  16003  odd2np1lem  16049  ndvdssub  16118  bitsinv1  16149  eucalglt  16290  hashgcdeq  16490  ramcl2lem  16710  ramcl  16730  cshwrepswhash1  16804  imasaddfnlem  17239  fnhomeqhomf  17400  initoeu2lem1  17729  cat1lem  17811  posi  18035  sgrp2nmndlem3  18564  dfgrp2  18604  grpidinv  18635  dfgrp3lem  18673  orbsta  18919  symgfvne  18988  symgfix2  19024  odlem1  19143  gexlem1  19184  slwispgp  19216  sylow3lem6  19237  efgrelexlemb  19356  gsumval3lem2  19507  pgpfac1  19683  pgpfaclem2  19685  pgpfac  19687  ablfaclem1  19688  isdomn  20565  obsip  20928  uvcval  20992  mvrval  21190  mhpval  21330  coe1tmmul2  21447  coe1tmmul  21448  mat1comp  21589  mat1dimid  21623  scmateALT  21661  marrepval  21711  marepvval  21716  minmar1val  21797  gsummatr01  21808  t0sep  22475  t1sep2  22520  is2ndc  22597  kqt0lem  22887  isr0  22888  isufil2  23059  xmeteq0  23491  imasf1oxmet  23528  xrsxmet  23972  iccpnfcnv  24107  dyadmax  24762  dyadmbl  24764  dvfsumle  25185  dvfsumabs  25187  dvfsumlem1  25190  mdegle0  25242  fta1g  25332  ig1peu  25336  fta1  25468  aalioulem2  25493  efopn  25813  efrlim  26119  musum  26340  dvdsmulf1o  26343  dchrsum2  26416  sumdchr2  26418  gausslemma2dlem0i  26512  addsqnreup  26591  2sqreulem1  26594  2sqreultblem  26596  2sqreunnlem1  26597  2sqreunnltblem  26599  2sqreulem3  26601  axtgcgrid  26824  axtgbtwnid  26827  tglowdim1i  26862  islmib  27148  axcontlem12  27343  upgredgpr  27512  ushgredgedg  27596  ushgredgedgloop  27598  rusgrpropnb  27950  rgrx0ndm  27960  uspgr2wlkeq  28013  wlkson  28024  upgrwlkdvdelem  28104  spthonepeq  28120  iswwlksnon  28218  wlklnwwlkln2lem  28247  wwlksnredwwlkn  28260  wwlksnextprop  28277  wwlksnwwlksnon  28280  elwwlks2ons3  28320  rusgrnumwwlklem  28335  clwlkclwwlklem2a4  28361  clwwlkn  28390  clwwlkext2edg  28420  hashecclwwlkn1  28441  umgrhashecclwwlk  28442  clwwlknon  28454  clwwlk0on0  28456  uhgr3cyclexlem  28545  1conngr  28558  frgr3vlem1  28637  3vfriswmgrlem  28641  frgrwopreglem3  28678  fusgreg2wsplem  28697  fusgreghash2wsp  28702  numclwlk1lem1  28733  numclwwlkovq  28738  numclwwlk2lem1  28740  frgrregord013  28759  friendshipgt3  28762  ex-opab  28796  isgrpoi  28860  grpoidinv2  28877  hvsubeq0  29430  hvaddcan  29432  hvsubadd  29439  normsub0  29498  omlsi  29766  pjoml  29798  nonbooli  30013  pj11  30076  lnopeq  30371  nmopun  30376  pjclem4a  30560  pj3lem1  30568  strlem4  30616  hstrlem4  30624  jplem1  30630  superpos  30716  ifeqeqx  30885  disji2f  30916  disjif2  30920  disjabrex  30921  disjabrexf  30922  disjxpin  30927  disjunsn  30933  ofpreima  31002  fgreu  31009  fcnvgreu  31010  gsumhashmul  31316  ismxidl  31634  xrge0iifcnv  31883  esumpr2  32035  eulerpartlemgvv  32343  eulerpartlemgh  32345  eulerpartlemgs2  32347  sgnsub  32511  plymulx0  32526  lpadmax  32662  lpadright  32664  bnj1321  33007  f1resfz0f1d  33072  subfacp1lem3  33144  pconncn  33186  cnpconn  33192  txpconn  33194  connpconn  33197  cvmlift3lem2  33282  cvmlift3lem4  33284  cvmlift3  33290  snmlflim  33294  iota5f  33669  sltres  33865  nosupprefixmo  33903  noinfprefixmo  33904  nosupcbv  33905  nosupno  33906  nosupfv  33909  noinfcbv  33920  noinfno  33921  noinffv  33924  elmade  34051  rankeq1o  34473  nn0prpw  34512  bj-csbsnlem  35088  bj-elgab  35127  bj-restsnss  35254  bj-restsnss2  35255  bj-imdirco  35361  fin2so  35764  poimirlem2  35779  poimirlem18  35795  poimirlem21  35798  poimirlem25  35802  poimirlem26  35803  poimirlem27  35804  mblfinlem2  35815  mbfresfi  35823  cnambfre  35825  ftc1anclem8  35857  fdc  35903  istotbnd  35927  isexid2  36013  isgrpda  36113  ismaxidl  36198  mpobi123f  36320  mptbi12f  36324  qsdisjALTV  36728  lsatcmp  37017  lshpkrlem1  37124  trlval2  38177  cdlemg1cex  38602  cdlemm10N  39132  dicval  39190  lcmineqlem4  40040  isdomn4  40172  fsuppind  40279  nnn1suc  40296  resubval  40350  unxpwdom3  40920  dgraalem  40970  dgraaub  40973  frege104  41575  pm13.192  42028  2sbc6g  42033  2sbc5g  42034  pm14.122b  42041  equncomVD  42488  csbingVD  42504  csbsngVD  42513  csbxpgVD  42514  csbresgVD  42515  csbrngVD  42516  csbima12gALTVD  42517  csbunigVD  42518  csbfv12gALTVD  42519  relopabVD  42521  dvnprodlem1  43487  dvnprodlem2  43488  dvnprodlem3  43489  dvnprod  43490  fourierdlem42  43690  etransclem11  43786  etransclem12  43787  etransclem33  43808  nnfoctbdjlem  43993  hoimbl  44169  cfsetsnfsetf  44552  aiota0def  44588  euoreqb  44601  funressndmafv2rn  44715  funressnbrafv2  44736  dfatbrafv2b  44737  funbrafv2  44739  fnbrafv2b  44740  elsetpreimafvbi  44843  elsetpreimafveq  44849  imasetpreimafvbijlemfo  44857  fargshiftf1  44893  ichnreuop  44924  paireqne  44963  reupr  44974  uspgrsprf1  45309  uspgrsprfo  45310  lidldomn1  45479  nn0sumshdiglem2  45968  mof0  46165  eufsnlem  46168  isthincd2lem1  46308  setrec2lem2  46400