Theorem eqeq2 2774

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  eqeq2i  2775  eqtr3  2784  clelab  2906  alexeqg  3610  pm13.183  3625  elab6g  3628  eqeu  3669  moeq3  3675  mo2icl  3677  mob2  3678  euind  3687  reu6i  3691  reu2eqd  3699  reuind  3716  sbc2or  3753  sbc5ALT  3773  csbiebg  3884  eqif  4522  sneq  4592  reusngf  4633  rexreusng  4638  reuprg0  4661  preq1b  4804  preq12bg  4811  preqsn  4820  disji2  5084  disjprg  5096  dtruALT  5345  opth  5444  euotd  5482  solin  5582  ideqg  5823  resieq  5976  cnveqb  6183  cnveq0  6184  reu3op  6279  reuop  6280  iota5  6504  funopg  6555  fneq2  6613  foeq3  6776  tz6.12f  6892  funbrfv  6915  fnbrfvb  6917  fvelimab  6939  elrnrexdm  7070  funsndifnop  7134  fconst5  7190  eufnfv  7213  f1veqaeq  7240  fpropnf1  7251  nf1const  7288  isosolem  7331  f1opr  7452  mpoeq123  7468  ovmpt4g  7543  ov3  7559  ovg  7561  caovcang  7597  caovcan  7600  tfisi  7839  tfindsg  7841  findsg  7878  f1oweALT  7953  seqomlem2  8422  oawordeu  8524  omopth  8632  ereq2  8687  qsdisj  8776  eroveu  8794  2dom  9011  fundmen  9012  xpf1o  9111  nneneq  9174  pwfir  9261  cantnflem1  9644  brttrcl  9668  ttrcltr  9671  ttrclss  9675  ttrclselem2  9681  updjud  9892  alephfp  10064  dfac5  10085  cardcf  10208  cfeq0  10213  sornom  10234  fpwwe2cbv  10588  fpwwe2lem3  10591  ltsosr  11052  map2psrpr  11068  axpre-lttri  11123  subval  11421  divval  11847  nn0ind-raph  12673  fvf1tp  13799  uzrdgfni  13971  sqeqor  14229  nn0opth2  14285  hashrabsn1  14387  elprchashprn2  14409  hashbclem  14465  hashbc  14466  hash2prde  14483  hash2pwpr  14489  brfi1indALT  14523  wrdind  14735  wrd2ind  14736  reuccatpfxs1lem  14759  cshf1  14823  wrdl3s3  14975  relexpindlem  15076  sgnsub  15119  sqrtval  15264  sqrmo  15278  reusq0  15492  summolem2  15743  prodmolem2  15965  divides  16288  dvdstr  16328  odd2np1lem  16374  ndvdssub  16443  bitsinv1  16476  eucalglt  16619  hashgcdeq  16825  ramcl2lem  17045  ramcl  17065  cshwrepswhash1  17138  imasaddfnlem  17558  fnhomeqhomf  17723  initoeu2lem1  18047  cat1lem  18129  posi  18349  sgrp2nmndlem3  18962  dfgrp2  19004  grpidinv  19040  dfgrp3lem  19080  orbsta  19353  symgfvne  19421  symgfix2  19456  odlem1  19575  gexlem1  19619  slwispgp  19651  sylow3lem6  19672  efgrelexlemb  19790  gsumval3lem2  19946  pgpfac1  20122  pgpfaclem2  20124  pgpfac  20126  ablfaclem1  20127  isdomn  20755  isdomn4  20766  domnlcanb  20770  domnrcanb  20772  obsip  21773  uvcval  21837  mvrval  22033  mhpval  22204  psdfval  22223  psdmvr  22234  coe1tmmul2  22339  coe1tmmul  22340  mat1comp  22500  mat1dimid  22534  scmateALT  22572  marrepval  22622  marepvval  22627  minmar1val  22708  gsummatr01  22719  t0sep  23384  t1sep2  23429  is2ndc  23506  kqt0lem  23796  isr0  23797  isufil2  23968  xmeteq0  24398  imasf1oxmet  24435  xrsxmet  24870  iccpnfcnv  25006  dyadmax  25660  dyadmbl  25662  dvfsumle  26083  dvfsumabs  26085  dvfsumlem1  26088  mdegle0  26137  fta1g  26230  ig1peu  26235  plyn0mulidp  26345  fta1  26372  aalioulem2  26397  taylthlem2  26437  efopn  26723  efrlim  27034  musum  27255  mpodvdsmulf1o  27258  dvdsmulf1o  27260  dchrsum2  27332  sumdchr2  27334  gausslemma2dlem0i  27428  addsqnreup  27507  2sqreulem1  27510  2sqreultblem  27512  2sqreunnlem1  27513  2sqreunnltblem  27515  2sqreulem3  27517  ltsres  27726  nosupprefixmo  27764  noinfprefixmo  27765  nosupcbv  27766  nosupno  27767  nosupfv  27770  noinfcbv  27781  noinfno  27782  noinffv  27785  elmade  27950  divsval  28282  noseqrdgfn  28399  bdayn0sf1o  28463  bdayfinbndlem2  28561  axtgcgrid  28632  axtgbtwnid  28635  tglowdim1i  28670  islmib  28960  axcontlem12  29176  upgredgpr  29343  ushgredgedg  29430  ushgredgedgloop  29432  rusgrpropnb  29784  rgrx0ndm  29794  uspgr2wlkeq  29846  wlkson  29855  upgrwlkdvdelem  29936  spthonepeq  29952  iswwlksnon  30053  wlklnwwlkln2lem  30082  wwlksnredwwlkn  30095  wwlksnextprop  30112  wwlksnwwlksnon  30115  elwwlks2ons3  30155  rusgrnumwwlklem  30173  clwlkclwwlklem2a4  30199  clwwlkn  30228  clwwlkext2edg  30258  hashecclwwlkn1  30279  umgrhashecclwwlk  30280  clwwlknon  30292  clwwlk0on0  30294  uhgr3cyclexlem  30383  1conngr  30396  frgr3vlem1  30475  3vfriswmgrlem  30479  frgrwopreglem3  30516  fusgreg2wsplem  30535  fusgreghash2wsp  30540  numclwlk1lem1  30571  numclwwlkovq  30576  numclwwlk2lem1  30578  frgrregord013  30597  friendshipgt3  30600  ex-opab  30634  isgrpoi  30701  grpoidinv2  30718  hvsubeq0  31271  hvaddcan  31273  hvsubadd  31280  normsub0  31339  omlsi  31607  pjoml  31639  nonbooli  31854  pj11  31917  lnopeq  32212  nmopun  32217  pjclem4a  32401  pj3lem1  32409  strlem4  32457  hstrlem4  32465  jplem1  32471  superpos  32557  ifeqeqx  32741  disji2f  32777  disjif2  32781  disjabrex  32782  disjabrexf  32783  disjxpin  32788  disjunsn  32794  ofpreima  32867  fgreu  32873  fcnvgreu  32874  gsumhashmul  33247  elrgspnlem2  33424  elrgspnlem3  33425  elrgspnlem4  33426  domnlcanOLD  33464  ismxidl  33650  mplasclco  33813  mplmulmvr  33836  psrmonmul2  33848  esplyfval  33860  esplyfval0  33861  esplyfv  33867  esplyfval3  33869  esplyfvaln  33871  xrge0iifcnv  34230  esumpr2  34364  eulerpartlemgvv  34673  eulerpartlemgh  34675  eulerpartlemgs2  34677  lpadmax  34979  lpadright  34981  bnj1321  35322  f1resfz0f1d  35464  subfacp1lem3  35532  pconncn  35574  cnpconn  35580  txpconn  35582  connpconn  35585  cvmlift3lem2  35670  cvmlift3lem4  35672  cvmlift3  35678  snmlflim  35682  iota5f  36074  rankeq1o  36521  nn0prpw  36683  tr0elw  36844  tr0el  36845  dfttc4lem1  36888  elttcirr  36891  bj-csbsnlem  37388  bj-elgab  37424  bj-restsnss  37573  bj-restsnss2  37574  bj-imdirco  37682  wl-isseteq  37999  wl-ax12v2cl  38000  wl-dfcleq  38008  fin2so  38106  poimirlem2  38121  poimirlem18  38137  poimirlem21  38140  poimirlem25  38144  poimirlem26  38145  poimirlem27  38146  mblfinlem2  38157  mbfresfi  38165  cnambfre  38167  ftc1anclem8  38199  fdc  38244  istotbnd  38268  isexid2  38354  isgrpda  38454  ismaxidl  38539  mpobi123f  38661  mptbi12f  38665  disjressuc2  38910  qsdisjALTV  39198  parteq2  39377  lsatcmp  39627  lshpkrlem1  39734  trlval2  40787  cdlemg1cex  41212  cdlemm10N  41742  dicval  41800  lcmineqlem4  42649  grpods  42811  unitscyglem2  42813  unitscyglem3  42814  unitscyglem4  42815  exfinfldd  42820  nnn1suc  42881  resubval  42976  redivvald  43051  fsuppind  43172  unxpwdom3  43672  dgraalem  43722  dgraaub  43725  onsucf1lem  43846  frege104  44543  pm13.192  44986  2sbc6g  44991  2sbc5g  44992  pm14.122b  44999  equncomVD  45443  csbingVD  45459  csbsngVD  45468  csbxpgVD  45469  csbresgVD  45470  csbrngVD  45471  csbima12gALTVD  45472  csbunigVD  45473  csbfv12gALTVD  45474  relopabVD  45476  dvnprodlem1  46520  dvnprodlem2  46521  dvnprodlem3  46522  dvnprod  46523  fourierdlem42  46723  etransclem11  46819  etransclem12  46820  etransclem33  46841  nnfoctbdjlem  47029  hoimbl  47205  cfsetsnfsetf  47652  aiota0def  47690  euoreqb  47703  funressndmafv2rn  47817  funressnbrafv2  47838  dfatbrafv2b  47839  funbrafv2  47841  fnbrafv2b  47842  elsetpreimafvbi  47997  elsetpreimafveq  48003  imasetpreimafvbijlemfo  48011  fargshiftf1  48047  ichnreuop  48078  paireqne  48117  reupr  48128  isuspgrim0  48516  upgrimpths  48531  clnbgrgrim  48556  grimedg  48557  isubgr3stgrlem4  48591  isubgr3stgrlem7  48594  gpgedg2ov  48688  gpgedg2iv  48689  pgnbgreunbgrlem1  48735  pgnbgreunbgrlem2lem3  48738  pgnbgreunbgrlem4  48741  pgnbgreunbgr  48747  uspgrsprf1  48769  uspgrsprfo  48770  lidldomn1  48853  nn0sumshdiglem2  49244  mof0  49459  eufsnlem  49462  oppcmndclem  49638  isthincd2lem1  50046  termcbasmo  50104  termcarweu  50149  arweuthinc  50150  arweutermc  50151  setrec2lem2  50315