Theorem eqeq2 2749

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqeq2i  2750  eqtr3  2759  clelab  2881  alexeqg  3594  pm13.183  3609  elab6g  3612  eqeu  3653  moeq3  3659  mo2icl  3661  mob2  3662  euind  3671  reu6i  3675  reu2eqd  3683  reuind  3700  sbc2or  3738  sbc5ALT  3758  csbiebg  3870  eqif  4509  sneq  4578  reusngf  4619  rexreusng  4624  reuprg0  4647  preq1b  4790  preq12bg  4797  preqsn  4806  disji2  5070  disjprg  5082  dtruALT  5323  opth  5422  euotd  5459  solin  5557  ideqg  5798  resieq  5947  cnveqb  6152  cnveq0  6153  reu3op  6248  reuop  6249  iota5  6473  funopg  6524  fneq2  6582  foeq3  6742  tz6.12f  6857  funbrfv  6880  fnbrfvb  6882  fvelimab  6904  elrnrexdm  7033  funsndifnop  7096  fconst5  7152  eufnfv  7175  f1veqaeq  7202  fpropnf1  7213  nf1const  7250  isosolem  7293  f1opr  7414  mpoeq123  7430  ovmpt4g  7505  ov3  7521  ovg  7523  caovcang  7559  caovcan  7562  tfisi  7801  tfindsg  7803  findsg  7839  f1oweALT  7916  seqomlem2  8381  oawordeu  8481  omopth  8589  ereq2  8643  qsdisj  8732  eroveu  8750  2dom  8968  fundmen  8969  xpf1o  9068  nneneq  9131  pwfir  9218  cantnflem1  9599  brttrcl  9623  ttrcltr  9626  ttrclss  9630  ttrclselem2  9636  updjud  9847  alephfp  10019  dfac5  10040  cardcf  10163  cfeq0  10167  sornom  10188  fpwwe2cbv  10542  fpwwe2lem3  10545  ltsosr  11006  map2psrpr  11022  axpre-lttri  11077  subval  11373  divval  11800  nn0ind-raph  12618  fvf1tp  13737  uzrdgfni  13909  sqeqor  14167  nn0opth2  14223  hashrabsn1  14325  elprchashprn2  14347  hashbclem  14403  hashbc  14404  hash2prde  14421  hash2pwpr  14427  brfi1indALT  14461  wrdind  14673  wrd2ind  14674  reuccatpfxs1lem  14697  cshf1  14761  wrdl3s3  14913  relexpindlem  15014  sqrtval  15188  sqrmo  15202  reusq0  15416  summolem2  15667  prodmolem2  15889  divides  16212  dvdstr  16252  odd2np1lem  16298  ndvdssub  16367  bitsinv1  16400  eucalglt  16543  hashgcdeq  16749  ramcl2lem  16969  ramcl  16989  cshwrepswhash1  17062  imasaddfnlem  17481  fnhomeqhomf  17646  initoeu2lem1  17970  cat1lem  18052  posi  18272  sgrp2nmndlem3  18885  dfgrp2  18927  grpidinv  18963  dfgrp3lem  19003  orbsta  19277  symgfvne  19345  symgfix2  19380  odlem1  19499  gexlem1  19543  slwispgp  19575  sylow3lem6  19596  efgrelexlemb  19714  gsumval3lem2  19870  pgpfac1  20046  pgpfaclem2  20048  pgpfac  20050  ablfaclem1  20051  isdomn  20671  isdomn4  20682  domnlcanb  20686  domnrcanb  20688  obsip  21709  uvcval  21773  mvrval  21969  mhpval  22114  psdfval  22133  psdmvr  22144  coe1tmmul2  22250  coe1tmmul  22251  mat1comp  22414  mat1dimid  22448  scmateALT  22486  marrepval  22536  marepvval  22541  minmar1val  22622  gsummatr01  22633  t0sep  23298  t1sep2  23343  is2ndc  23420  kqt0lem  23710  isr0  23711  isufil2  23882  xmeteq0  24312  imasf1oxmet  24349  xrsxmet  24784  iccpnfcnv  24920  dyadmax  25574  dyadmbl  25576  dvfsumle  25998  dvfsumleOLD  25999  dvfsumabs  26001  dvfsumlem1  26004  mdegle0  26054  fta1g  26147  ig1peu  26152  fta1  26287  aalioulem2  26312  taylthlem2  26353  efopn  26638  efrlim  26950  efrlimOLD  26951  musum  27172  mpodvdsmulf1o  27175  dvdsmulf1o  27177  dchrsum2  27250  sumdchr2  27252  gausslemma2dlem0i  27346  addsqnreup  27425  2sqreulem1  27428  2sqreultblem  27430  2sqreunnlem1  27431  2sqreunnltblem  27433  2sqreulem3  27435  ltsres  27645  nosupprefixmo  27683  noinfprefixmo  27684  nosupcbv  27685  nosupno  27686  nosupfv  27689  noinfcbv  27700  noinfno  27701  noinffv  27704  elmade  27868  divsval  28200  noseqrdgfn  28317  bdayn0sf1o  28381  bdayfinbndlem2  28479  axtgcgrid  28550  axtgbtwnid  28553  tglowdim1i  28588  islmib  28874  axcontlem12  29063  upgredgpr  29230  ushgredgedg  29317  ushgredgedgloop  29319  rusgrpropnb  29672  rgrx0ndm  29682  uspgr2wlkeq  29734  wlkson  29743  upgrwlkdvdelem  29824  spthonepeq  29840  iswwlksnon  29941  wlklnwwlkln2lem  29970  wwlksnredwwlkn  29983  wwlksnextprop  30000  wwlksnwwlksnon  30003  elwwlks2ons3  30043  rusgrnumwwlklem  30061  clwlkclwwlklem2a4  30087  clwwlkn  30116  clwwlkext2edg  30146  hashecclwwlkn1  30167  umgrhashecclwwlk  30168  clwwlknon  30180  clwwlk0on0  30182  uhgr3cyclexlem  30271  1conngr  30284  frgr3vlem1  30363  3vfriswmgrlem  30367  frgrwopreglem3  30404  fusgreg2wsplem  30423  fusgreghash2wsp  30428  numclwlk1lem1  30459  numclwwlkovq  30464  numclwwlk2lem1  30466  frgrregord013  30485  friendshipgt3  30488  ex-opab  30522  isgrpoi  30589  grpoidinv2  30606  hvsubeq0  31159  hvaddcan  31161  hvsubadd  31168  normsub0  31227  omlsi  31495  pjoml  31527  nonbooli  31742  pj11  31805  lnopeq  32100  nmopun  32105  pjclem4a  32289  pj3lem1  32297  strlem4  32345  hstrlem4  32353  jplem1  32359  superpos  32445  ifeqeqx  32632  disji2f  32667  disjif2  32671  disjabrex  32672  disjabrexf  32673  disjxpin  32678  disjunsn  32684  ofpreima  32758  fgreu  32764  fcnvgreu  32765  sgnsub  32930  gsumhashmul  33148  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  domnlcanOLD  33361  ismxidl  33542  mplmulmvr  33703  psrmonmul2  33715  esplyfval  33727  esplyfval0  33728  esplyfv  33734  esplyfval3  33736  esplyfvaln  33738  xrge0iifcnv  34098  esumpr2  34232  eulerpartlemgvv  34541  eulerpartlemgh  34543  eulerpartlemgs2  34545  plymulx0  34712  lpadmax  34847  lpadright  34849  bnj1321  35190  f1resfz0f1d  35317  subfacp1lem3  35385  pconncn  35427  cnpconn  35433  txpconn  35435  connpconn  35438  cvmlift3lem2  35523  cvmlift3lem4  35525  cvmlift3  35531  snmlflim  35535  iota5f  35927  rankeq1o  36374  nn0prpw  36526  tr0elw  36687  tr0el  36688  dfttc4lem1  36731  elttcirr  36734  bj-csbsnlem  37223  bj-elgab  37259  bj-restsnss  37408  bj-restsnss2  37409  bj-imdirco  37517  wl-isseteq  37832  wl-ax12v2cl  37833  wl-dfcleq  37841  fin2so  37939  poimirlem2  37954  poimirlem18  37970  poimirlem21  37973  poimirlem25  37977  poimirlem26  37978  poimirlem27  37979  mblfinlem2  37990  mbfresfi  37998  cnambfre  38000  ftc1anclem8  38032  fdc  38077  istotbnd  38101  isexid2  38187  isgrpda  38287  ismaxidl  38372  mpobi123f  38494  mptbi12f  38498  disjressuc2  38743  qsdisjALTV  39031  parteq2  39210  lsatcmp  39460  lshpkrlem1  39567  trlval2  40620  cdlemg1cex  41045  cdlemm10N  41575  dicval  41633  lcmineqlem4  42482  grpods  42644  unitscyglem2  42646  unitscyglem3  42647  unitscyglem4  42648  exfinfldd  42653  nnn1suc  42715  resubval  42810  redivvald  42885  fsuppind  43034  unxpwdom3  43538  dgraalem  43588  dgraaub  43591  onsucf1lem  43712  frege104  44409  pm13.192  44852  2sbc6g  44857  2sbc5g  44858  pm14.122b  44865  equncomVD  45309  csbingVD  45325  csbsngVD  45334  csbxpgVD  45335  csbresgVD  45336  csbrngVD  45337  csbima12gALTVD  45338  csbunigVD  45339  csbfv12gALTVD  45340  relopabVD  45342  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  dvnprod  46392  fourierdlem42  46592  etransclem11  46688  etransclem12  46689  etransclem33  46710  nnfoctbdjlem  46898  hoimbl  47074  cfsetsnfsetf  47503  aiota0def  47541  euoreqb  47554  funressndmafv2rn  47668  funressnbrafv2  47689  dfatbrafv2b  47690  funbrafv2  47692  fnbrafv2b  47693  elsetpreimafvbi  47848  elsetpreimafveq  47854  imasetpreimafvbijlemfo  47862  fargshiftf1  47898  ichnreuop  47929  paireqne  47968  reupr  47979  isuspgrim0  48367  upgrimpths  48382  clnbgrgrim  48407  grimedg  48408  isubgr3stgrlem4  48442  isubgr3stgrlem7  48445  gpgedg2ov  48539  gpgedg2iv  48540  pgnbgreunbgrlem1  48586  pgnbgreunbgrlem2lem3  48589  pgnbgreunbgrlem4  48592  pgnbgreunbgr  48598  uspgrsprf1  48620  uspgrsprfo  48621  lidldomn1  48704  nn0sumshdiglem2  49095  mof0  49310  eufsnlem  49313  oppcmndclem  49489  isthincd2lem1  49897  termcbasmo  49955  termcarweu  50000  arweuthinc  50001  arweutermc  50002  setrec2lem2  50166