Theorem eqeq2 2742

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqeq2i  2743  eqtr3  2752  clelab  2874  alexeqg  3620  pm13.183  3635  elab6g  3638  eqeu  3679  moeq3  3685  mo2icl  3687  mob2  3688  euind  3697  reu6i  3701  reu2eqd  3709  reuind  3726  sbc2or  3764  sbc5ALT  3784  csbiebg  3896  eqif  4532  sneq  4601  reusngf  4640  rexreusng  4645  reuprg0  4668  preq1b  4812  preq12bg  4819  preqsn  4828  disji2  5093  disjprg  5105  dtruALT  5345  opth  5438  euotd  5475  solin  5575  ideqg  5817  resieq  5963  cnveqb  6171  cnveq0  6172  reu3op  6267  reuop  6268  iota5  6496  funopg  6552  fneq2  6612  foeq3  6772  tz6.12f  6886  funbrfv  6911  fnbrfvb  6913  fvelimab  6935  elrnrexdm  7063  funsndifnop  7125  fconst5  7182  eufnfv  7205  f1veqaeq  7233  fpropnf1  7244  nf1const  7281  isosolem  7324  f1opr  7447  mpoeq123  7463  ovmpt4g  7538  ov3  7554  ovg  7556  caovcang  7592  caovcan  7595  tfisi  7837  tfindsg  7839  findsg  7875  f1oweALT  7953  seqomlem2  8421  oawordeu  8521  omopth  8628  ereq2  8681  qsdisj  8769  eroveu  8787  2dom  9003  fundmen  9004  xpf1o  9108  nneneq  9175  pwfir  9272  cantnflem1  9648  brttrcl  9672  ttrcltr  9675  ttrclss  9679  ttrclselem2  9685  updjud  9893  alephfp  10067  dfac5  10088  cardcf  10211  cfeq0  10215  sornom  10236  fpwwe2cbv  10589  fpwwe2lem3  10592  ltsosr  11053  map2psrpr  11069  axpre-lttri  11124  subval  11418  divval  11845  nn0ind-raph  12640  fvf1tp  13757  uzrdgfni  13929  sqeqor  14187  nn0opth2  14243  hashrabsn1  14345  elprchashprn2  14367  hashbclem  14423  hashbc  14424  hash2prde  14441  hash2pwpr  14447  brfi1indALT  14481  wrdind  14693  wrd2ind  14694  reuccatpfxs1lem  14717  cshf1  14781  wrdl3s3  14934  relexpindlem  15035  sqrtval  15209  sqrmo  15223  reusq0  15437  summolem2  15688  prodmolem2  15907  divides  16230  dvdstr  16270  odd2np1lem  16316  ndvdssub  16385  bitsinv1  16418  eucalglt  16561  hashgcdeq  16766  ramcl2lem  16986  ramcl  17006  cshwrepswhash1  17079  imasaddfnlem  17497  fnhomeqhomf  17658  initoeu2lem1  17982  cat1lem  18064  posi  18284  sgrp2nmndlem3  18858  dfgrp2  18900  grpidinv  18936  dfgrp3lem  18976  orbsta  19251  symgfvne  19317  symgfix2  19352  odlem1  19471  gexlem1  19515  slwispgp  19547  sylow3lem6  19568  efgrelexlemb  19686  gsumval3lem2  19842  pgpfac1  20018  pgpfaclem2  20020  pgpfac  20022  ablfaclem1  20023  isdomn  20620  isdomn4  20631  domnlcanb  20635  domnrcanb  20637  obsip  21636  uvcval  21700  mvrval  21897  mhpval  22032  psdfval  22051  psdmvr  22062  coe1tmmul2  22168  coe1tmmul  22169  mat1comp  22333  mat1dimid  22367  scmateALT  22405  marrepval  22455  marepvval  22460  minmar1val  22541  gsummatr01  22552  t0sep  23217  t1sep2  23262  is2ndc  23339  kqt0lem  23629  isr0  23630  isufil2  23801  xmeteq0  24232  imasf1oxmet  24269  xrsxmet  24704  iccpnfcnv  24848  dyadmax  25505  dyadmbl  25507  dvfsumle  25932  dvfsumleOLD  25933  dvfsumabs  25935  dvfsumlem1  25938  mdegle0  25988  fta1g  26081  ig1peu  26086  fta1  26222  aalioulem2  26247  taylthlem2  26288  efopn  26573  efrlim  26885  efrlimOLD  26886  musum  27107  mpodvdsmulf1o  27110  dvdsmulf1o  27112  dchrsum2  27185  sumdchr2  27187  gausslemma2dlem0i  27281  addsqnreup  27360  2sqreulem1  27363  2sqreultblem  27365  2sqreunnlem1  27366  2sqreunnltblem  27368  2sqreulem3  27370  sltres  27580  nosupprefixmo  27618  noinfprefixmo  27619  nosupcbv  27620  nosupno  27621  nosupfv  27624  noinfcbv  27635  noinfno  27636  noinffv  27639  elmade  27785  divsval  28098  noseqrdgfn  28206  bdayn0sf1o  28265  axtgcgrid  28396  axtgbtwnid  28399  tglowdim1i  28434  islmib  28720  axcontlem12  28908  upgredgpr  29075  ushgredgedg  29162  ushgredgedgloop  29164  rusgrpropnb  29517  rgrx0ndm  29527  uspgr2wlkeq  29580  wlkson  29590  upgrwlkdvdelem  29672  spthonepeq  29688  iswwlksnon  29789  wlklnwwlkln2lem  29818  wwlksnredwwlkn  29831  wwlksnextprop  29848  wwlksnwwlksnon  29851  elwwlks2ons3  29891  rusgrnumwwlklem  29906  clwlkclwwlklem2a4  29932  clwwlkn  29961  clwwlkext2edg  29991  hashecclwwlkn1  30012  umgrhashecclwwlk  30013  clwwlknon  30025  clwwlk0on0  30027  uhgr3cyclexlem  30116  1conngr  30129  frgr3vlem1  30208  3vfriswmgrlem  30212  frgrwopreglem3  30249  fusgreg2wsplem  30268  fusgreghash2wsp  30273  numclwlk1lem1  30304  numclwwlkovq  30309  numclwwlk2lem1  30311  frgrregord013  30330  friendshipgt3  30333  ex-opab  30367  isgrpoi  30433  grpoidinv2  30450  hvsubeq0  31003  hvaddcan  31005  hvsubadd  31012  normsub0  31071  omlsi  31339  pjoml  31371  nonbooli  31586  pj11  31649  lnopeq  31944  nmopun  31949  pjclem4a  32133  pj3lem1  32141  strlem4  32189  hstrlem4  32197  jplem1  32203  superpos  32289  ifeqeqx  32477  disji2f  32512  disjif2  32516  disjabrex  32517  disjabrexf  32518  disjxpin  32523  disjunsn  32529  ofpreima  32595  fgreu  32602  fcnvgreu  32603  sgnsub  32768  gsumhashmul  33007  elrgspnlem2  33200  elrgspnlem3  33201  elrgspnlem4  33202  domnlcanOLD  33236  ismxidl  33439  xrge0iifcnv  33929  esumpr2  34063  eulerpartlemgvv  34373  eulerpartlemgh  34375  eulerpartlemgs2  34377  plymulx0  34544  lpadmax  34679  lpadright  34681  bnj1321  35023  f1resfz0f1d  35101  subfacp1lem3  35169  pconncn  35211  cnpconn  35217  txpconn  35219  connpconn  35222  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3  35315  snmlflim  35319  iota5f  35706  rankeq1o  36154  nn0prpw  36306  bj-csbsnlem  36886  bj-elgab  36922  bj-restsnss  37066  bj-restsnss2  37067  bj-imdirco  37173  wl-isseteq  37488  wl-ax12v2cl  37489  fin2so  37596  poimirlem2  37611  poimirlem18  37627  poimirlem21  37630  poimirlem25  37634  poimirlem26  37635  poimirlem27  37636  mblfinlem2  37647  mbfresfi  37655  cnambfre  37657  ftc1anclem8  37689  fdc  37734  istotbnd  37758  isexid2  37844  isgrpda  37944  ismaxidl  38029  mpobi123f  38151  mptbi12f  38155  disjressuc2  38369  qsdisjALTV  38601  parteq2  38762  lsatcmp  38991  lshpkrlem1  39098  trlval2  40152  cdlemg1cex  40577  cdlemm10N  41107  dicval  41165  lcmineqlem4  42015  grpods  42177  unitscyglem2  42179  unitscyglem3  42180  unitscyglem4  42181  exfinfldd  42186  nnn1suc  42249  resubval  42350  redivvald  42425  fsuppind  42571  unxpwdom3  43077  dgraalem  43127  dgraaub  43130  onsucf1lem  43251  frege104  43949  pm13.192  44392  2sbc6g  44397  2sbc5g  44398  pm14.122b  44405  equncomVD  44850  csbingVD  44866  csbsngVD  44875  csbxpgVD  44876  csbresgVD  44877  csbrngVD  44878  csbima12gALTVD  44879  csbunigVD  44880  csbfv12gALTVD  44881  relopabVD  44883  dvnprodlem1  45937  dvnprodlem2  45938  dvnprodlem3  45939  dvnprod  45940  fourierdlem42  46140  etransclem11  46236  etransclem12  46237  etransclem33  46258  nnfoctbdjlem  46446  hoimbl  46622  cfsetsnfsetf  47049  aiota0def  47087  euoreqb  47100  funressndmafv2rn  47214  funressnbrafv2  47235  dfatbrafv2b  47236  funbrafv2  47238  fnbrafv2b  47239  elsetpreimafvbi  47382  elsetpreimafveq  47388  imasetpreimafvbijlemfo  47396  fargshiftf1  47432  ichnreuop  47463  paireqne  47502  reupr  47513  isuspgrim0  47884  upgrimpths  47899  clnbgrgrim  47924  grimedg  47925  isubgr3stgrlem4  47958  isubgr3stgrlem7  47961  gpgedg2ov  48047  gpgedg2iv  48048  pgnbgreunbgrlem1  48093  pgnbgreunbgrlem2lem3  48096  pgnbgreunbgrlem4  48099  pgnbgreunbgr  48105  uspgrsprf1  48125  uspgrsprfo  48126  lidldomn1  48209  nn0sumshdiglem2  48601  mof0  48816  eufsnlem  48819  oppcmndclem  48996  isthincd2lem1  49404  termcbasmo  49462  termcarweu  49507  arweuthinc  49508  arweutermc  49509  setrec2lem2  49673