Theorem eqeq2 2773

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 2772	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 2155  ax-ext 2733

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

This theorem is used by:  eqeq2i  2774  eqtr3  2783  clelab  2905  alexeqg  3605  pm13.183  3620  elab6g  3623  eqeu  3664  moeq3  3670  mo2icl  3672  mob2  3673  euind  3682  reu6i  3686  reu2eqd  3694  reuind  3711  sbc2or  3748  sbc5ALT  3768  csbiebg  3879  eqif  4524  sneq  4594  reusngf  4635  rexreusng  4640  reuprg0  4663  preq1b  4806  preq12bg  4813  preqsn  4822  disji2  5087  disjprg  5099  dtruALT  5350  opth  5445  euotd  5486  solin  5586  ideqg  5829  resieq  5981  cnveqb  6190  cnveq0  6191  reu3op  6295  reuop  6296  iota5  6521  funopg  6574  fneq2  6631  foeq3  6794  tz6.12f  6910  funbrfv  6933  fnbrfvb  6935  fvelimab  6957  elrnrexdm  7089  funsndifnop  7155  fconst5  7212  eufnfv  7235  f1veqaeq  7260  fpropnf1  7271  nf1const  7312  isosolem  7355  f1opr  7476  mpoeq123  7492  ovmpt4g  7567  ov3  7583  ovg  7585  caovcang  7622  caovcan  7625  tfisi  7870  tfindsg  7872  findsg  7909  f1oweALT  7984  seqomlem2  8461  oawordeu  8563  omopth  8671  ereq2  8726  qsdisj  8815  eroveu  8833  2dom  9058  fundmen  9059  xpf1o  9158  nneneq  9221  pwfir  9308  cantnflem1  9690  brttrcl  9714  ttrcltr  9717  ttrclss  9721  ttrclselem2  9727  setrec2lem2  9976  updjud  10015  alephfp  10187  dfac5  10207  cardcf  10329  cfeq0  10334  sornom  10355  fpwwe2cbv  10715  fpwwe2lem3  10718  ltsosr  11179  map2psrpr  11195  axpre-lttri  11250  subval  11548  divval  11976  nn0ind-raph  12799  f1resfz0f1d  13927  fvf1tp  13929  uzrdgfni  14101  sqeqor  14360  nn0opth2  14416  hashrabsn1  14518  elprchashprn2  14540  hashbclem  14597  hashbc  14598  hash2prde  14615  hash2pwpr  14621  brfi1indALT  14655  wrdind  14871  wrd2ind  14872  reuccatpfxs1lem  14895  cshf1  14961  wrdl3s3  15115  relexpindlem  15216  sgnsub  15259  sqrtval  15404  sqrmo  15418  reusq0  15632  summolem2  15882  prodmolem2  16102  divides  16424  dvdstr  16464  odd2np1lem  16510  ndvdssub  16579  bitsinv1  16612  eucalglt  16760  hashgcdeq  16967  ramcl2lem  17187  ramcl  17207  cshwrepswhash1  17280  imasaddfnlem  17700  fnhomeqhomf  17865  initoeu2lem1  18189  cat1lem  18271  posi  18491  sgrp2nmndlem3  19124  degenmgm2nfun  19139  dfgrp2  19173  grpidinv  19209  dfgrp3lem  19248  orbsta  19527  symgfvne  19595  symgfix2  19630  odlem1  19749  gexlem1  19793  slwispgp  19825  sylow3lem6  19846  efgrelexlemb  19964  gsumval3lem2  20120  pgpfac1  20296  pgpfaclem2  20298  pgpfac  20300  ablfaclem1  20301  isdomn  20957  isdomn4  20967  domnlcanb  20971  domnrcanb  20973  obsip  22027  uvcval  22091  mvrval  22289  mhpval  22460  psdfval  22479  psdmvr  22490  coe1tmmul2  22595  coe1tmmul  22596  mat1comp  22755  mat1dimid  22789  scmateALT  22827  marrepval  22877  marepvval  22882  minmar1val  22963  gsummatr01  22974  t0sep  23642  t1sep2  23687  is2ndc  23764  kqt0lem  24055  isr0  24056  isufil2  24227  xmeteq0  24657  imasf1oxmet  24694  xrsxmet  25129  iccpnfcnv  25265  dyadmax  25919  dyadmbl  25921  dvfsumle  26341  dvfsumabs  26343  dvfsumlem1  26346  mdegle0  26395  fta1g  26488  ig1peu  26493  plyn0mulidp  26602  fta1  26629  aalioulem2  26660  taylthlem2  26701  efopn  26986  efrlim  27297  musum  27518  mpodvdsmulf1o  27521  dvdsmulf1o  27523  dchrsum2  27595  sumdchr2  27597  gausslemma2dlem0i  27691  addsqnreup  27770  2sqreulem1  27773  2sqreultblem  27775  2sqreunnlem1  27776  2sqreunnltblem  27778  2sqreulem3  27780  ltsres  28019  nosupprefixmo  28057  noinfprefixmo  28058  nosupcbv  28059  nosupno  28060  nosupfv  28063  noinfcbv  28074  noinfno  28075  noinffv  28078  elmade  28243  divsval  28575  noseqrdgfn  28692  bdayn0sf1o  28756  bdayfinbndlem2  28854  axtgcgrid  28925  axtgbtwnid  28928  tglowdim1i  28964  islmib  29292  prlngmo2  29434  axcontlem12  29553  upgredgpr  29720  ushgredgedg  29810  ushgredgedgloop  29812  rusgrpropnb  30164  rgrx0ndm  30174  uspgr2wlkeq  30226  wlkson  30235  upgrwlkdvdelem  30322  spthonepeq  30338  iswwlksnon  30442  wlklnwwlkln2lem  30471  wwlksnredwwlkn  30484  wwlksnextprop  30501  wwlksnwwlksnon  30504  elwwlks2ons3  30544  rusgrnumwwlklem  30562  clwlkclwwlklem2a4  30588  clwwlkn  30617  clwwlkext2edg  30647  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  clwwlknon  30681  clwwlk0on0  30683  uhgr3cyclexlem  30782  1conngr  30795  frgr3vlem1  30874  3vfriswmgrlem  30878  frgrwopreglem3  30915  fusgreg2wsplem  30934  fusgreghash2wsp  30939  numclwlk1lem1  30970  numclwwlkovq  30975  numclwwlk2lem1  30977  frgrregord013  30996  friendshipgt3  30999  ex-opab  31033  isgrpoi  31100  grpoidinv2  31117  hvsubeq0  31670  hvaddcan  31672  hvsubadd  31679  normsub0  31738  omlsi  32006  pjoml  32038  nonbooli  32253  pj11  32316  lnopeq  32611  nmopun  32616  pjclem4a  32800  pj3lem1  32808  strlem4  32856  hstrlem4  32864  jplem1  32870  superpos  32956  ifeqeqx  33138  disji2f  33171  disjif2  33175  disjabrex  33176  disjabrexf  33177  disjxpin  33182  disjunsn  33188  ofpreima  33259  fgreu  33265  fcnvgreu  33266  gsumhashmul  33628  elrgspnlem2  33804  elrgspnlem3  33805  elrgspnlem4  33806  ismxidl  33987  mplasclco  34148  mplmulmvr  34171  psrmonmul2  34183  esplyfval  34195  esplyfval0  34196  esplyfv  34202  esplyfval3  34204  esplyfvaln  34206  xrge0iifcnv  34565  esumpr2  34699  eulerpartlemgvv  35008  eulerpartlemgh  35010  eulerpartlemgs2  35012  lpadmax  35314  lpadright  35316  bnj1321  35657  subfacp1lem3  35947  pconncn  35989  cnpconn  35995  txpconn  35997  connpconn  36000  cvmlift3lem2  36085  cvmlift3lem4  36087  cvmlift3  36093  snmlflim  36097  iota5f  36489  rankeq1o  36932  nn0prpw  37111  tr0elw  37272  tr0el  37273  dfttc4lem1  37316  elttcirr  37319  bj-csbsnlem  37815  bj-elgab  37852  bj-restsnss  38004  bj-restsnss2  38005  bj-imdirco  38111  wl-isseteq  38428  wl-ax12v2cl  38429  wl-dfcleq  38437  fin2so  38530  poimirlem2  38540  poimirlem18  38556  poimirlem21  38559  poimirlem25  38563  poimirlem26  38564  poimirlem27  38565  mblfinlem2  38576  mbfresfi  38584  cnambfre  38586  ftc1anclem8  38618  findcard4  38632  fdc  38679  istotbnd  38703  isexid2  38789  isgrpda  38889  ismaxidl  38974  mpobi123f  39094  mptbi12f  39098  disjressuc2  39343  qsdisjALTV  39631  parteq2  39810  lsatcmp  40060  lshpkrlem1  40167  trlval2  41220  cdlemg1cex  41645  cdlemm10N  42175  dicval  42233  lcmineqlem4  43082  grpods  43244  unitscyglem2  43246  unitscyglem3  43247  unitscyglem4  43248  exfinfldd  43253  nnn1suc  43331  resubval  43418  redivvald  43493  fsuppind  43618  unxpwdom3  44096  dgraalem  44146  dgraaub  44149  onsucf1lem  44270  frege104  44966  pm13.192  45393  2sbc6g  45398  2sbc5g  45399  pm14.122b  45406  equncomVD  45849  csbingVD  45865  csbsngVD  45874  csbxpgVD  45875  csbresgVD  45876  csbrngVD  45877  csbima12gALTVD  45878  csbunigVD  45879  csbfv12gALTVD  45880  relopabVD  45882  dvnprodlem1  46955  dvnprodlem2  46956  dvnprodlem3  46957  dvnprod  46958  fourierdlem42  47158  etransclem11  47254  etransclem12  47255  etransclem33  47276  nnfoctbdjlem  47464  hoimbl  47640  cfsetsnfsetf  48127  aiota0def  48165  euoreqb  48178  funressndmafv2rn  48292  funressnbrafv2  48313  dfatbrafv2b  48314  funbrafv2  48316  fnbrafv2b  48317  elsetpreimafvbi  48472  elsetpreimafveq  48478  imasetpreimafvbijlemfo  48486  fargshiftf1  48522  ichnreuop  48553  paireqne  48592  reupr  48603  isuspgrim0  48991  upgrimpths  49006  clnbgrgrim  49031  grimedg  49032  isubgr3stgrlem4  49066  isubgr3stgrlem7  49069  gpgedg2ov  49163  gpgedg2iv  49164  pgnbgreunbgrlem1  49210  pgnbgreunbgrlem2lem3  49213  pgnbgreunbgrlem4  49216  pgnbgreunbgr  49222  uspgrsprf1  49244  uspgrsprfo  49245  lidldomn1  49327  nn0sumshdiglem2  49733  mof0  49947  eufsnlem  49950  oppcmndclem  50124  isthincd2lem1  50532  termcbasmo  50590  termcarweu  50635  arweuthinc  50636  arweutermc  50637