Theorem eqeq2 2748

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 2747	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 2708

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

This theorem is referenced by:  eqeq2i  2749  eqtr3  2758  clelab  2880  alexeqg  3593  pm13.183  3608  elab6g  3611  eqeu  3652  moeq3  3658  mo2icl  3660  mob2  3661  euind  3670  reu6i  3674  reu2eqd  3682  reuind  3699  sbc2or  3737  sbc5ALT  3757  csbiebg  3869  eqif  4508  sneq  4577  reusngf  4618  rexreusng  4623  reuprg0  4646  preq1b  4789  preq12bg  4796  preqsn  4805  disji2  5069  disjprg  5081  dtruALT  5330  opth  5429  euotd  5467  solin  5566  ideqg  5806  resieq  5955  cnveqb  6160  cnveq0  6161  reu3op  6256  reuop  6257  iota5  6481  funopg  6532  fneq2  6590  foeq3  6750  tz6.12f  6865  funbrfv  6888  fnbrfvb  6890  fvelimab  6912  elrnrexdm  7041  funsndifnop  7105  fconst5  7161  eufnfv  7184  f1veqaeq  7211  fpropnf1  7222  nf1const  7259  isosolem  7302  f1opr  7423  mpoeq123  7439  ovmpt4g  7514  ov3  7530  ovg  7532  caovcang  7568  caovcan  7571  tfisi  7810  tfindsg  7812  findsg  7848  f1oweALT  7925  seqomlem2  8390  oawordeu  8490  omopth  8598  ereq2  8652  qsdisj  8741  eroveu  8759  2dom  8977  fundmen  8978  xpf1o  9077  nneneq  9140  pwfir  9227  cantnflem1  9610  brttrcl  9634  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  updjud  9858  alephfp  10030  dfac5  10051  cardcf  10174  cfeq0  10178  sornom  10199  fpwwe2cbv  10553  fpwwe2lem3  10556  ltsosr  11017  map2psrpr  11033  axpre-lttri  11088  subval  11384  divval  11811  nn0ind-raph  12629  fvf1tp  13748  uzrdgfni  13920  sqeqor  14178  nn0opth2  14234  hashrabsn1  14336  elprchashprn2  14358  hashbclem  14414  hashbc  14415  hash2prde  14432  hash2pwpr  14438  brfi1indALT  14472  wrdind  14684  wrd2ind  14685  reuccatpfxs1lem  14708  cshf1  14772  wrdl3s3  14924  relexpindlem  15025  sqrtval  15199  sqrmo  15213  reusq0  15427  summolem2  15678  prodmolem2  15900  divides  16223  dvdstr  16263  odd2np1lem  16309  ndvdssub  16378  bitsinv1  16411  eucalglt  16554  hashgcdeq  16760  ramcl2lem  16980  ramcl  17000  cshwrepswhash1  17073  imasaddfnlem  17492  fnhomeqhomf  17657  initoeu2lem1  17981  cat1lem  18063  posi  18283  sgrp2nmndlem3  18896  dfgrp2  18938  grpidinv  18974  dfgrp3lem  19014  orbsta  19288  symgfvne  19356  symgfix2  19391  odlem1  19510  gexlem1  19554  slwispgp  19586  sylow3lem6  19607  efgrelexlemb  19725  gsumval3lem2  19881  pgpfac1  20057  pgpfaclem2  20059  pgpfac  20061  ablfaclem1  20062  isdomn  20682  isdomn4  20693  domnlcanb  20697  domnrcanb  20699  obsip  21701  uvcval  21765  mvrval  21960  mhpval  22105  psdfval  22124  psdmvr  22135  coe1tmmul2  22241  coe1tmmul  22242  mat1comp  22405  mat1dimid  22439  scmateALT  22477  marrepval  22527  marepvval  22532  minmar1val  22613  gsummatr01  22624  t0sep  23289  t1sep2  23334  is2ndc  23411  kqt0lem  23701  isr0  23702  isufil2  23873  xmeteq0  24303  imasf1oxmet  24340  xrsxmet  24775  iccpnfcnv  24911  dyadmax  25565  dyadmbl  25567  dvfsumle  25988  dvfsumabs  25990  dvfsumlem1  25993  mdegle0  26042  fta1g  26135  ig1peu  26140  fta1  26274  aalioulem2  26299  taylthlem2  26339  efopn  26622  efrlim  26933  musum  27154  mpodvdsmulf1o  27157  dvdsmulf1o  27159  dchrsum2  27231  sumdchr2  27233  gausslemma2dlem0i  27327  addsqnreup  27406  2sqreulem1  27409  2sqreultblem  27411  2sqreunnlem1  27412  2sqreunnltblem  27414  2sqreulem3  27416  ltsres  27626  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupno  27667  nosupfv  27670  noinfcbv  27681  noinfno  27682  noinffv  27685  elmade  27849  divsval  28181  noseqrdgfn  28298  bdayn0sf1o  28362  bdayfinbndlem2  28460  axtgcgrid  28531  axtgbtwnid  28534  tglowdim1i  28569  islmib  28855  axcontlem12  29044  upgredgpr  29211  ushgredgedg  29298  ushgredgedgloop  29300  rusgrpropnb  29652  rgrx0ndm  29662  uspgr2wlkeq  29714  wlkson  29723  upgrwlkdvdelem  29804  spthonepeq  29820  iswwlksnon  29921  wlklnwwlkln2lem  29950  wwlksnredwwlkn  29963  wwlksnextprop  29980  wwlksnwwlksnon  29983  elwwlks2ons3  30023  rusgrnumwwlklem  30041  clwlkclwwlklem2a4  30067  clwwlkn  30096  clwwlkext2edg  30126  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwwlknon  30160  clwwlk0on0  30162  uhgr3cyclexlem  30251  1conngr  30264  frgr3vlem1  30343  3vfriswmgrlem  30347  frgrwopreglem3  30384  fusgreg2wsplem  30403  fusgreghash2wsp  30408  numclwlk1lem1  30439  numclwwlkovq  30444  numclwwlk2lem1  30446  frgrregord013  30465  friendshipgt3  30468  ex-opab  30502  isgrpoi  30569  grpoidinv2  30586  hvsubeq0  31139  hvaddcan  31141  hvsubadd  31148  normsub0  31207  omlsi  31475  pjoml  31507  nonbooli  31722  pj11  31785  lnopeq  32080  nmopun  32085  pjclem4a  32269  pj3lem1  32277  strlem4  32325  hstrlem4  32333  jplem1  32339  superpos  32425  ifeqeqx  32612  disji2f  32647  disjif2  32651  disjabrex  32652  disjabrexf  32653  disjxpin  32658  disjunsn  32664  ofpreima  32738  fgreu  32744  fcnvgreu  32745  sgnsub  32910  gsumhashmul  33128  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  domnlcanOLD  33341  ismxidl  33522  mplmulmvr  33683  psrmonmul2  33695  esplyfval  33707  esplyfval0  33708  esplyfv  33714  esplyfval3  33716  esplyfvaln  33718  xrge0iifcnv  34077  esumpr2  34211  eulerpartlemgvv  34520  eulerpartlemgh  34522  eulerpartlemgs2  34524  plymulx0  34691  lpadmax  34826  lpadright  34828  bnj1321  35169  f1resfz0f1d  35296  subfacp1lem3  35364  pconncn  35406  cnpconn  35412  txpconn  35414  connpconn  35417  cvmlift3lem2  35502  cvmlift3lem4  35504  cvmlift3  35510  snmlflim  35514  iota5f  35906  rankeq1o  36353  nn0prpw  36505  tr0elw  36666  tr0el  36667  dfttc4lem1  36710  elttcirr  36713  bj-csbsnlem  37210  bj-elgab  37246  bj-restsnss  37395  bj-restsnss2  37396  bj-imdirco  37504  wl-isseteq  37821  wl-ax12v2cl  37822  wl-dfcleq  37830  fin2so  37928  poimirlem2  37943  poimirlem18  37959  poimirlem21  37962  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  mblfinlem2  37979  mbfresfi  37987  cnambfre  37989  ftc1anclem8  38021  fdc  38066  istotbnd  38090  isexid2  38176  isgrpda  38276  ismaxidl  38361  mpobi123f  38483  mptbi12f  38487  disjressuc2  38732  qsdisjALTV  39020  parteq2  39199  lsatcmp  39449  lshpkrlem1  39556  trlval2  40609  cdlemg1cex  41034  cdlemm10N  41564  dicval  41622  lcmineqlem4  42471  grpods  42633  unitscyglem2  42635  unitscyglem3  42636  unitscyglem4  42637  exfinfldd  42642  nnn1suc  42704  resubval  42799  redivvald  42874  fsuppind  43023  unxpwdom3  43523  dgraalem  43573  dgraaub  43576  onsucf1lem  43697  frege104  44394  pm13.192  44837  2sbc6g  44842  2sbc5g  44843  pm14.122b  44850  equncomVD  45294  csbingVD  45310  csbsngVD  45319  csbxpgVD  45320  csbresgVD  45321  csbrngVD  45322  csbima12gALTVD  45323  csbunigVD  45324  csbfv12gALTVD  45325  relopabVD  45327  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  dvnprod  46377  fourierdlem42  46577  etransclem11  46673  etransclem12  46674  etransclem33  46695  nnfoctbdjlem  46883  hoimbl  47059  cfsetsnfsetf  47506  aiota0def  47544  euoreqb  47557  funressndmafv2rn  47671  funressnbrafv2  47692  dfatbrafv2b  47693  funbrafv2  47695  fnbrafv2b  47696  elsetpreimafvbi  47851  elsetpreimafveq  47857  imasetpreimafvbijlemfo  47865  fargshiftf1  47901  ichnreuop  47932  paireqne  47971  reupr  47982  isuspgrim0  48370  upgrimpths  48385  clnbgrgrim  48410  grimedg  48411  isubgr3stgrlem4  48445  isubgr3stgrlem7  48448  gpgedg2ov  48542  gpgedg2iv  48543  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem4  48595  pgnbgreunbgr  48601  uspgrsprf1  48623  uspgrsprfo  48624  lidldomn1  48707  nn0sumshdiglem2  49098  mof0  49313  eufsnlem  49316  oppcmndclem  49492  isthincd2lem1  49900  termcbasmo  49958  termcarweu  50003  arweuthinc  50004  arweutermc  50005  setrec2lem2  50169