Theorem eqeq2 2777

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  eqeq2i  2778  eqtr3  2787  clelab  2909  alexeqg  3612  pm13.183  3627  elab6g  3630  eqeu  3671  moeq3  3677  mo2icl  3679  mob2  3680  euind  3689  reu6i  3693  reu2eqd  3701  reuind  3718  sbc2or  3755  sbc5ALT  3775  csbiebg  3886  eqif  4531  sneq  4601  reusngf  4642  rexreusng  4647  reuprg0  4670  preq1b  4813  preq12bg  4820  preqsn  4829  disji2  5095  disjprg  5107  dtruALT  5361  opth  5460  euotd  5498  solin  5598  ideqg  5839  resieq  5991  cnveqb  6197  cnveq0  6198  reu3op  6297  reuop  6298  iota5  6523  funopg  6574  fneq2  6631  foeq3  6794  tz6.12f  6910  funbrfv  6933  fnbrfvb  6935  fvelimab  6957  elrnrexdm  7088  funsndifnop  7154  fconst5  7211  eufnfv  7234  f1veqaeq  7259  fpropnf1  7270  nf1const  7311  isosolem  7354  f1opr  7475  mpoeq123  7491  ovmpt4g  7566  ov3  7582  ovg  7584  caovcang  7621  caovcan  7624  tfisi  7861  tfindsg  7863  findsg  7900  f1oweALT  7975  seqomlem2  8444  oawordeu  8546  omopth  8654  ereq2  8709  qsdisj  8798  eroveu  8816  2dom  9034  fundmen  9035  xpf1o  9134  nneneq  9197  pwfir  9283  cantnflem1  9665  brttrcl  9689  ttrcltr  9692  ttrclss  9696  ttrclselem2  9702  updjud  9936  alephfp  10108  dfac5  10128  cardcf  10250  cfeq0  10255  sornom  10276  fpwwe2cbv  10630  fpwwe2lem3  10633  ltsosr  11094  map2psrpr  11110  axpre-lttri  11165  subval  11463  divval  11889  nn0ind-raph  12712  f1resfz0f1d  13838  fvf1tp  13840  uzrdgfni  14012  sqeqor  14270  nn0opth2  14326  hashrabsn1  14428  elprchashprn2  14450  hashbclem  14507  hashbc  14508  hash2prde  14525  hash2pwpr  14531  brfi1indALT  14565  wrdind  14781  wrd2ind  14782  reuccatpfxs1lem  14805  cshf1  14871  wrdl3s3  15023  relexpindlem  15124  sgnsub  15167  sqrtval  15312  sqrmo  15326  reusq0  15540  summolem2  15790  prodmolem2  16012  divides  16334  dvdstr  16374  odd2np1lem  16420  ndvdssub  16489  bitsinv1  16522  eucalglt  16665  hashgcdeq  16871  ramcl2lem  17091  ramcl  17111  cshwrepswhash1  17184  imasaddfnlem  17604  fnhomeqhomf  17769  initoeu2lem1  18093  cat1lem  18175  posi  18395  sgrp2nmndlem3  19024  degenmgm2nfun  19039  dfgrp2  19073  grpidinv  19109  dfgrp3lem  19148  orbsta  19427  symgfvne  19495  symgfix2  19530  odlem1  19649  gexlem1  19693  slwispgp  19725  sylow3lem6  19746  efgrelexlemb  19864  gsumval3lem2  20020  pgpfac1  20196  pgpfaclem2  20198  pgpfac  20200  ablfaclem1  20201  isdomn  20854  isdomn4  20864  domnlcanb  20868  domnrcanb  20870  obsip  21921  uvcval  21985  mvrval  22181  mhpval  22352  psdfval  22371  psdmvr  22382  coe1tmmul2  22487  coe1tmmul  22488  mat1comp  22647  mat1dimid  22681  scmateALT  22719  marrepval  22769  marepvval  22774  minmar1val  22855  gsummatr01  22866  t0sep  23531  t1sep2  23576  is2ndc  23653  kqt0lem  23944  isr0  23945  isufil2  24116  xmeteq0  24546  imasf1oxmet  24583  xrsxmet  25018  iccpnfcnv  25154  dyadmax  25808  dyadmbl  25810  dvfsumle  26231  dvfsumabs  26233  dvfsumlem1  26236  mdegle0  26285  fta1g  26378  ig1peu  26383  plyn0mulidp  26493  fta1  26520  aalioulem2  26547  taylthlem2  26588  efopn  26874  efrlim  27185  musum  27406  mpodvdsmulf1o  27409  dvdsmulf1o  27411  dchrsum2  27483  sumdchr2  27485  gausslemma2dlem0i  27579  addsqnreup  27658  2sqreulem1  27661  2sqreultblem  27663  2sqreunnlem1  27664  2sqreunnltblem  27666  2sqreulem3  27668  ltsres  27877  nosupprefixmo  27915  noinfprefixmo  27916  nosupcbv  27917  nosupno  27918  nosupfv  27921  noinfcbv  27932  noinfno  27933  noinffv  27936  elmade  28101  divsval  28433  noseqrdgfn  28550  bdayn0sf1o  28614  bdayfinbndlem2  28712  axtgcgrid  28783  axtgbtwnid  28786  tglowdim1i  28821  islmib  29147  prlngmo2  29261  axcontlem12  29380  upgredgpr  29547  ushgredgedg  29637  ushgredgedgloop  29639  rusgrpropnb  29991  rgrx0ndm  30001  uspgr2wlkeq  30053  wlkson  30062  upgrwlkdvdelem  30149  spthonepeq  30165  iswwlksnon  30269  wlklnwwlkln2lem  30298  wwlksnredwwlkn  30311  wwlksnextprop  30328  wwlksnwwlksnon  30331  elwwlks2ons3  30371  rusgrnumwwlklem  30389  clwlkclwwlklem2a4  30415  clwwlkn  30444  clwwlkext2edg  30474  hashecclwwlkn1  30495  umgrhashecclwwlk  30496  clwwlknon  30508  clwwlk0on0  30510  uhgr3cyclexlem  30603  1conngr  30616  frgr3vlem1  30695  3vfriswmgrlem  30699  frgrwopreglem3  30736  fusgreg2wsplem  30755  fusgreghash2wsp  30760  numclwlk1lem1  30791  numclwwlkovq  30796  numclwwlk2lem1  30798  frgrregord013  30817  friendshipgt3  30820  ex-opab  30854  isgrpoi  30921  grpoidinv2  30938  hvsubeq0  31491  hvaddcan  31493  hvsubadd  31500  normsub0  31559  omlsi  31827  pjoml  31859  nonbooli  32074  pj11  32137  lnopeq  32432  nmopun  32437  pjclem4a  32621  pj3lem1  32629  strlem4  32677  hstrlem4  32685  jplem1  32691  superpos  32777  ifeqeqx  32959  disji2f  32993  disjif2  32997  disjabrex  32998  disjabrexf  32999  disjxpin  33004  disjunsn  33010  ofpreima  33081  fgreu  33087  fcnvgreu  33088  gsumhashmul  33451  elrgspnlem2  33627  elrgspnlem3  33628  elrgspnlem4  33629  ismxidl  33809  mplasclco  33970  mplmulmvr  33993  psrmonmul2  34005  esplyfval  34017  esplyfval0  34018  esplyfv  34024  esplyfval3  34026  esplyfvaln  34028  xrge0iifcnv  34387  esumpr2  34521  eulerpartlemgvv  34831  eulerpartlemgh  34833  eulerpartlemgs2  34835  lpadmax  35137  lpadright  35139  bnj1321  35480  subfacp1lem3  35711  pconncn  35753  cnpconn  35759  txpconn  35761  connpconn  35764  cvmlift3lem2  35849  cvmlift3lem4  35851  cvmlift3  35857  snmlflim  35861  iota5f  36253  rankeq1o  36700  nn0prpw  36891  tr0elw  37052  tr0el  37053  dfttc4lem1  37096  elttcirr  37099  bj-csbsnlem  37595  bj-elgab  37632  bj-restsnss  37782  bj-restsnss2  37783  bj-imdirco  37891  wl-isseteq  38208  wl-ax12v2cl  38209  wl-dfcleq  38217  fin2so  38315  poimirlem2  38330  poimirlem18  38346  poimirlem21  38349  poimirlem25  38353  poimirlem26  38354  poimirlem27  38355  mblfinlem2  38366  mbfresfi  38374  cnambfre  38376  ftc1anclem8  38408  findcard4  38422  fdc  38454  istotbnd  38478  isexid2  38564  isgrpda  38664  ismaxidl  38749  mpobi123f  38869  mptbi12f  38873  disjressuc2  39118  qsdisjALTV  39406  parteq2  39585  lsatcmp  39835  lshpkrlem1  39942  trlval2  40995  cdlemg1cex  41420  cdlemm10N  41950  dicval  42008  lcmineqlem4  42857  grpods  43019  unitscyglem2  43021  unitscyglem3  43022  unitscyglem4  43023  exfinfldd  43028  nnn1suc  43091  resubval  43186  redivvald  43261  fsuppind  43380  unxpwdom3  43880  dgraalem  43930  dgraaub  43933  onsucf1lem  44054  frege104  44751  pm13.192  45178  2sbc6g  45183  2sbc5g  45184  pm14.122b  45191  equncomVD  45634  csbingVD  45650  csbsngVD  45659  csbxpgVD  45660  csbresgVD  45661  csbrngVD  45662  csbima12gALTVD  45663  csbunigVD  45664  csbfv12gALTVD  45665  relopabVD  45667  dvnprodlem1  46718  dvnprodlem2  46719  dvnprodlem3  46720  dvnprod  46721  fourierdlem42  46921  etransclem11  47017  etransclem12  47018  etransclem33  47039  nnfoctbdjlem  47227  hoimbl  47403  cfsetsnfsetf  47853  aiota0def  47891  euoreqb  47904  funressndmafv2rn  48018  funressnbrafv2  48039  dfatbrafv2b  48040  funbrafv2  48042  fnbrafv2b  48043  elsetpreimafvbi  48198  elsetpreimafveq  48204  imasetpreimafvbijlemfo  48212  fargshiftf1  48248  ichnreuop  48279  paireqne  48318  reupr  48329  isuspgrim0  48717  upgrimpths  48732  clnbgrgrim  48757  grimedg  48758  isubgr3stgrlem4  48792  isubgr3stgrlem7  48795  gpgedg2ov  48889  gpgedg2iv  48890  pgnbgreunbgrlem1  48936  pgnbgreunbgrlem2lem3  48939  pgnbgreunbgrlem4  48942  pgnbgreunbgr  48948  uspgrsprf1  48970  uspgrsprfo  48971  lidldomn1  49053  nn0sumshdiglem2  49459  mof0  49673  eufsnlem  49676  oppcmndclem  49852  isthincd2lem1  50260  termcbasmo  50318  termcarweu  50363  arweuthinc  50364  arweutermc  50365  setrec2lem2  50529