Theorem eqeq2 2772

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 2771	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 2732

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

This theorem is used by:  eqeq2i  2773  eqtr3  2782  clelab  2904  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  5353  opth  5452  euotd  5490  solin  5590  ideqg  5831  resieq  5983  cnveqb  6190  cnveq0  6191  reu3op  6290  reuop  6291  iota5  6516  funopg  6568  fneq2  6625  foeq3  6788  tz6.12f  6904  funbrfv  6927  fnbrfvb  6929  fvelimab  6951  elrnrexdm  7083  funsndifnop  7149  fconst5  7206  eufnfv  7229  f1veqaeq  7254  fpropnf1  7265  nf1const  7306  isosolem  7349  f1opr  7470  mpoeq123  7486  ovmpt4g  7561  ov3  7577  ovg  7579  caovcang  7616  caovcan  7619  tfisi  7856  tfindsg  7858  findsg  7895  f1oweALT  7970  seqomlem2  8441  oawordeu  8543  omopth  8651  ereq2  8706  qsdisj  8795  eroveu  8813  2dom  9038  fundmen  9039  xpf1o  9138  nneneq  9201  pwfir  9287  cantnflem1  9669  brttrcl  9693  ttrcltr  9696  ttrclss  9700  ttrclselem2  9706  updjud  9940  alephfp  10112  dfac5  10132  cardcf  10254  cfeq0  10259  sornom  10280  fpwwe2cbv  10640  fpwwe2lem3  10643  ltsosr  11104  map2psrpr  11120  axpre-lttri  11175  subval  11473  divval  11899  nn0ind-raph  12722  f1resfz0f1d  13849  fvf1tp  13851  uzrdgfni  14023  sqeqor  14281  nn0opth2  14337  hashrabsn1  14439  elprchashprn2  14461  hashbclem  14518  hashbc  14519  hash2prde  14536  hash2pwpr  14542  brfi1indALT  14576  wrdind  14792  wrd2ind  14793  reuccatpfxs1lem  14816  cshf1  14882  wrdl3s3  15036  relexpindlem  15137  sgnsub  15180  sqrtval  15325  sqrmo  15339  reusq0  15553  summolem2  15803  prodmolem2  16023  divides  16345  dvdstr  16385  odd2np1lem  16431  ndvdssub  16500  bitsinv1  16533  eucalglt  16676  hashgcdeq  16882  ramcl2lem  17102  ramcl  17122  cshwrepswhash1  17195  imasaddfnlem  17615  fnhomeqhomf  17780  initoeu2lem1  18104  cat1lem  18186  posi  18406  sgrp2nmndlem3  19038  degenmgm2nfun  19053  dfgrp2  19087  grpidinv  19123  dfgrp3lem  19162  orbsta  19441  symgfvne  19509  symgfix2  19544  odlem1  19663  gexlem1  19707  slwispgp  19739  sylow3lem6  19760  efgrelexlemb  19878  gsumval3lem2  20034  pgpfac1  20210  pgpfaclem2  20212  pgpfac  20214  ablfaclem1  20215  isdomn  20868  isdomn4  20878  domnlcanb  20882  domnrcanb  20884  obsip  21935  uvcval  21999  mvrval  22197  mhpval  22368  psdfval  22387  psdmvr  22398  coe1tmmul2  22503  coe1tmmul  22504  mat1comp  22663  mat1dimid  22697  scmateALT  22735  marrepval  22785  marepvval  22790  minmar1val  22871  gsummatr01  22882  t0sep  23550  t1sep2  23595  is2ndc  23672  kqt0lem  23963  isr0  23964  isufil2  24135  xmeteq0  24565  imasf1oxmet  24602  xrsxmet  25037  iccpnfcnv  25173  dyadmax  25827  dyadmbl  25829  dvfsumle  26249  dvfsumabs  26251  dvfsumlem1  26254  mdegle0  26303  fta1g  26396  ig1peu  26401  plyn0mulidp  26512  fta1  26539  aalioulem2  26570  taylthlem2  26611  efopn  26896  efrlim  27207  musum  27428  mpodvdsmulf1o  27431  dvdsmulf1o  27433  dchrsum2  27505  sumdchr2  27507  gausslemma2dlem0i  27601  addsqnreup  27680  2sqreulem1  27683  2sqreultblem  27685  2sqreunnlem1  27686  2sqreunnltblem  27688  2sqreulem3  27690  ltsres  27899  nosupprefixmo  27937  noinfprefixmo  27938  nosupcbv  27939  nosupno  27940  nosupfv  27943  noinfcbv  27954  noinfno  27955  noinffv  27958  elmade  28123  divsval  28455  noseqrdgfn  28572  bdayn0sf1o  28636  bdayfinbndlem2  28734  axtgcgrid  28805  axtgbtwnid  28808  tglowdim1i  28844  islmib  29172  prlngmo2  29314  axcontlem12  29433  upgredgpr  29600  ushgredgedg  29690  ushgredgedgloop  29692  rusgrpropnb  30044  rgrx0ndm  30054  uspgr2wlkeq  30106  wlkson  30115  upgrwlkdvdelem  30202  spthonepeq  30218  iswwlksnon  30322  wlklnwwlkln2lem  30351  wwlksnredwwlkn  30364  wwlksnextprop  30381  wwlksnwwlksnon  30384  elwwlks2ons3  30424  rusgrnumwwlklem  30442  clwlkclwwlklem2a4  30468  clwwlkn  30497  clwwlkext2edg  30527  hashecclwwlkn1  30548  umgrhashecclwwlk  30549  clwwlknon  30561  clwwlk0on0  30563  uhgr3cyclexlem  30662  1conngr  30675  frgr3vlem1  30754  3vfriswmgrlem  30758  frgrwopreglem3  30795  fusgreg2wsplem  30814  fusgreghash2wsp  30819  numclwlk1lem1  30850  numclwwlkovq  30855  numclwwlk2lem1  30857  frgrregord013  30876  friendshipgt3  30879  ex-opab  30913  isgrpoi  30980  grpoidinv2  30997  hvsubeq0  31550  hvaddcan  31552  hvsubadd  31559  normsub0  31618  omlsi  31886  pjoml  31918  nonbooli  32133  pj11  32196  lnopeq  32491  nmopun  32496  pjclem4a  32680  pj3lem1  32688  strlem4  32736  hstrlem4  32744  jplem1  32750  superpos  32836  ifeqeqx  33018  disji2f  33051  disjif2  33055  disjabrex  33056  disjabrexf  33057  disjxpin  33062  disjunsn  33068  ofpreima  33139  fgreu  33145  fcnvgreu  33146  gsumhashmul  33508  elrgspnlem2  33684  elrgspnlem3  33685  elrgspnlem4  33686  ismxidl  33866  mplasclco  34027  mplmulmvr  34050  psrmonmul2  34062  esplyfval  34074  esplyfval0  34075  esplyfv  34081  esplyfval3  34083  esplyfvaln  34085  xrge0iifcnv  34444  esumpr2  34578  eulerpartlemgvv  34888  eulerpartlemgh  34890  eulerpartlemgs2  34892  lpadmax  35194  lpadright  35196  bnj1321  35537  subfacp1lem3  35762  pconncn  35804  cnpconn  35810  txpconn  35812  connpconn  35815  cvmlift3lem2  35900  cvmlift3lem4  35902  cvmlift3  35908  snmlflim  35912  iota5f  36304  rankeq1o  36752  nn0prpw  36943  tr0elw  37104  tr0el  37105  dfttc4lem1  37148  elttcirr  37151  bj-csbsnlem  37647  bj-elgab  37684  bj-restsnss  37834  bj-restsnss2  37835  bj-imdirco  37943  wl-isseteq  38260  wl-ax12v2cl  38261  wl-dfcleq  38269  fin2so  38362  poimirlem2  38372  poimirlem18  38388  poimirlem21  38391  poimirlem25  38395  poimirlem26  38396  poimirlem27  38397  mblfinlem2  38408  mbfresfi  38416  cnambfre  38418  ftc1anclem8  38450  findcard4  38464  fdc  38496  istotbnd  38520  isexid2  38606  isgrpda  38706  ismaxidl  38791  mpobi123f  38911  mptbi12f  38915  disjressuc2  39160  qsdisjALTV  39448  parteq2  39627  lsatcmp  39877  lshpkrlem1  39984  trlval2  41037  cdlemg1cex  41462  cdlemm10N  41992  dicval  42050  lcmineqlem4  42899  grpods  43061  unitscyglem2  43063  unitscyglem3  43064  unitscyglem4  43065  exfinfldd  43070  nnn1suc  43148  resubval  43243  redivvald  43318  fsuppind  43437  unxpwdom3  43937  dgraalem  43987  dgraaub  43990  onsucf1lem  44111  frege104  44808  pm13.192  45235  2sbc6g  45240  2sbc5g  45241  pm14.122b  45248  equncomVD  45691  csbingVD  45707  csbsngVD  45716  csbxpgVD  45717  csbresgVD  45718  csbrngVD  45719  csbima12gALTVD  45720  csbunigVD  45721  csbfv12gALTVD  45722  relopabVD  45724  dvnprodlem1  46775  dvnprodlem2  46776  dvnprodlem3  46777  dvnprod  46778  fourierdlem42  46978  etransclem11  47074  etransclem12  47075  etransclem33  47096  nnfoctbdjlem  47284  hoimbl  47460  cfsetsnfsetf  47947  aiota0def  47985  euoreqb  47998  funressndmafv2rn  48112  funressnbrafv2  48133  dfatbrafv2b  48134  funbrafv2  48136  fnbrafv2b  48137  elsetpreimafvbi  48292  elsetpreimafveq  48298  imasetpreimafvbijlemfo  48306  fargshiftf1  48342  ichnreuop  48373  paireqne  48412  reupr  48423  isuspgrim0  48811  upgrimpths  48826  clnbgrgrim  48851  grimedg  48852  isubgr3stgrlem4  48886  isubgr3stgrlem7  48889  gpgedg2ov  48983  gpgedg2iv  48984  pgnbgreunbgrlem1  49030  pgnbgreunbgrlem2lem3  49033  pgnbgreunbgrlem4  49036  pgnbgreunbgr  49042  uspgrsprf1  49064  uspgrsprfo  49065  lidldomn1  49147  nn0sumshdiglem2  49553  mof0  49767  eufsnlem  49770  oppcmndclem  49944  isthincd2lem1  50352  termcbasmo  50410  termcarweu  50455  arweuthinc  50456  arweutermc  50457  setrec2lem2  50621