Theorem eqeq2 2743

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  eqeq2i  2744  eqeq12OLD  2750  eqtr3  2757  clelab  2878  alexeqg  3604  pm13.183  3621  elab6g  3624  eqeu  3667  moeq3  3673  mo2icl  3675  mob2  3676  euind  3685  reu6i  3689  reu2eqd  3697  reuind  3714  sbc2or  3751  sbc5ALT  3771  csbiebg  3891  eqif  4532  sneq  4601  reusngf  4638  rexreusng  4645  reuprg0  4668  preq1b  4809  preq12bg  4816  preqsn  4824  disji2  5092  disjprgw  5105  disjprg  5106  dtruALT  5348  opth  5438  euotd  5475  solin  5575  ideqg  5812  resieq  5953  cnveqb  6153  cnveq0  6154  reu3op  6249  reuop  6250  iota5  6484  funopg  6540  fneq2  6599  foeq3  6759  tz6.12f  6873  funbrfv  6898  fnbrfvb  6900  fvelimab  6919  elrnrexdm  7044  funsndifnop  7102  fconst5  7160  eufnfv  7184  f1veqaeq  7209  fpropnf1  7219  nf1const  7255  isosolem  7297  f1opr  7418  mpoeq123  7434  ovmpt4g  7507  ov3  7522  ovg  7524  caovcang  7560  caovcan  7563  tfisi  7800  tfindsg  7802  findsg  7841  f1oweALT  7910  seqomlem2  8402  oawordeu  8507  omopth  8613  ereq2  8663  qsdisj  8740  eroveu  8758  2dom  8981  fundmen  8982  xpf1o  9090  pwfir  9127  nneneq  9160  nneneqOLD  9172  cantnflem1  9634  brttrcl  9658  ttrcltr  9661  ttrclss  9665  ttrclselem2  9671  updjud  9879  alephfp  10053  dfac5  10073  cardcf  10197  cfeq0  10201  sornom  10222  fpwwe2cbv  10575  fpwwe2lem3  10578  ltsosr  11039  map2psrpr  11055  axpre-lttri  11110  subval  11401  divval  11824  nn0ind-raph  12612  uzrdgfni  13873  sqeqor  14130  nn0opth2  14182  hashrabsn1  14284  elprchashprn2  14306  hashbclem  14361  hashbc  14362  hash2prde  14381  hash2pwpr  14387  brfi1indALT  14411  wrdind  14622  wrd2ind  14623  reuccatpfxs1lem  14646  cshf1  14710  wrdl3s3  14863  relexpindlem  14960  sqrtval  15134  sqrmo  15148  reusq0  15359  summolem2  15612  prodmolem2  15829  divides  16149  dvdstr  16187  odd2np1lem  16233  ndvdssub  16302  bitsinv1  16333  eucalglt  16472  hashgcdeq  16672  ramcl2lem  16892  ramcl  16912  cshwrepswhash1  16986  imasaddfnlem  17424  fnhomeqhomf  17585  initoeu2lem1  17914  cat1lem  17996  posi  18220  sgrp2nmndlem3  18749  dfgrp2  18789  grpidinv  18821  dfgrp3lem  18859  orbsta  19107  symgfvne  19176  symgfix2  19212  odlem1  19331  gexlem1  19375  slwispgp  19407  sylow3lem6  19428  efgrelexlemb  19546  gsumval3lem2  19697  pgpfac1  19873  pgpfaclem2  19875  pgpfac  19877  ablfaclem1  19878  isdomn  20801  obsip  21164  uvcval  21228  mvrval  21427  mhpval  21567  coe1tmmul2  21684  coe1tmmul  21685  mat1comp  21826  mat1dimid  21860  scmateALT  21898  marrepval  21948  marepvval  21953  minmar1val  22034  gsummatr01  22045  t0sep  22712  t1sep2  22757  is2ndc  22834  kqt0lem  23124  isr0  23125  isufil2  23296  xmeteq0  23728  imasf1oxmet  23765  xrsxmet  24209  iccpnfcnv  24344  dyadmax  24999  dyadmbl  25001  dvfsumle  25422  dvfsumabs  25424  dvfsumlem1  25427  mdegle0  25479  fta1g  25569  ig1peu  25573  fta1  25705  aalioulem2  25730  efopn  26050  efrlim  26356  musum  26577  dvdsmulf1o  26580  dchrsum2  26653  sumdchr2  26655  gausslemma2dlem0i  26749  addsqnreup  26828  2sqreulem1  26831  2sqreultblem  26833  2sqreunnlem1  26834  2sqreunnltblem  26836  2sqreulem3  26838  sltres  27047  nosupprefixmo  27085  noinfprefixmo  27086  nosupcbv  27087  nosupno  27088  nosupfv  27091  noinfcbv  27102  noinfno  27103  noinffv  27106  elmade  27240  axtgcgrid  27468  axtgbtwnid  27471  tglowdim1i  27506  islmib  27792  axcontlem12  27987  upgredgpr  28156  ushgredgedg  28240  ushgredgedgloop  28242  rusgrpropnb  28594  rgrx0ndm  28604  uspgr2wlkeq  28657  wlkson  28667  upgrwlkdvdelem  28747  spthonepeq  28763  iswwlksnon  28861  wlklnwwlkln2lem  28890  wwlksnredwwlkn  28903  wwlksnextprop  28920  wwlksnwwlksnon  28923  elwwlks2ons3  28963  rusgrnumwwlklem  28978  clwlkclwwlklem2a4  29004  clwwlkn  29033  clwwlkext2edg  29063  hashecclwwlkn1  29084  umgrhashecclwwlk  29085  clwwlknon  29097  clwwlk0on0  29099  uhgr3cyclexlem  29188  1conngr  29201  frgr3vlem1  29280  3vfriswmgrlem  29284  frgrwopreglem3  29321  fusgreg2wsplem  29340  fusgreghash2wsp  29345  numclwlk1lem1  29376  numclwwlkovq  29381  numclwwlk2lem1  29383  frgrregord013  29402  friendshipgt3  29405  ex-opab  29439  isgrpoi  29503  grpoidinv2  29520  hvsubeq0  30073  hvaddcan  30075  hvsubadd  30082  normsub0  30141  omlsi  30409  pjoml  30441  nonbooli  30656  pj11  30719  lnopeq  31014  nmopun  31019  pjclem4a  31203  pj3lem1  31211  strlem4  31259  hstrlem4  31267  jplem1  31273  superpos  31359  ifeqeqx  31528  disji2f  31562  disjif2  31566  disjabrex  31567  disjabrexf  31568  disjxpin  31573  disjunsn  31579  ofpreima  31648  fgreu  31655  fcnvgreu  31656  gsumhashmul  31968  ismxidl  32307  xrge0iifcnv  32603  esumpr2  32755  eulerpartlemgvv  33065  eulerpartlemgh  33067  eulerpartlemgs2  33069  sgnsub  33233  plymulx0  33248  lpadmax  33384  lpadright  33386  bnj1321  33728  f1resfz0f1d  33793  subfacp1lem3  33863  pconncn  33905  cnpconn  33911  txpconn  33913  connpconn  33916  cvmlift3lem2  34001  cvmlift3lem4  34003  cvmlift3  34009  snmlflim  34013  iota5f  34382  rankeq1o  34832  nn0prpw  34871  bj-csbsnlem  35446  bj-elgab  35482  bj-restsnss  35627  bj-restsnss2  35628  bj-imdirco  35734  fin2so  36138  poimirlem2  36153  poimirlem18  36169  poimirlem21  36172  poimirlem25  36176  poimirlem26  36177  poimirlem27  36178  mblfinlem2  36189  mbfresfi  36197  cnambfre  36199  ftc1anclem8  36231  fdc  36277  istotbnd  36301  isexid2  36387  isgrpda  36487  ismaxidl  36572  mpobi123f  36694  mptbi12f  36698  disjressuc2  36923  qsdisjALTV  37150  parteq2  37310  lsatcmp  37538  lshpkrlem1  37645  trlval2  38699  cdlemg1cex  39124  cdlemm10N  39654  dicval  39712  lcmineqlem4  40562  isdomn4  40697  fsuppind  40823  nnn1suc  40840  resubval  40894  unxpwdom3  41480  dgraalem  41530  dgraaub  41533  onsucf1lem  41662  frege104  42361  pm13.192  42812  2sbc6g  42817  2sbc5g  42818  pm14.122b  42825  equncomVD  43272  csbingVD  43288  csbsngVD  43297  csbxpgVD  43298  csbresgVD  43299  csbrngVD  43300  csbima12gALTVD  43301  csbunigVD  43302  csbfv12gALTVD  43303  relopabVD  43305  dvnprodlem1  44307  dvnprodlem2  44308  dvnprodlem3  44309  dvnprod  44310  fourierdlem42  44510  etransclem11  44606  etransclem12  44607  etransclem33  44628  nnfoctbdjlem  44816  hoimbl  44992  cfsetsnfsetf  45412  aiota0def  45448  euoreqb  45461  funressndmafv2rn  45575  funressnbrafv2  45596  dfatbrafv2b  45597  funbrafv2  45599  fnbrafv2b  45600  elsetpreimafvbi  45703  elsetpreimafveq  45709  imasetpreimafvbijlemfo  45717  fargshiftf1  45753  ichnreuop  45784  paireqne  45823  reupr  45834  uspgrsprf1  46169  uspgrsprfo  46170  lidldomn1  46339  nn0sumshdiglem2  46828  mof0  47024  eufsnlem  47027  isthincd2lem1  47167  setrec2lem2  47259