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  5326  opth  5425  euotd  5462  solin  5560  ideqg  5801  resieq  5950  cnveqb  6155  cnveq0  6156  reu3op  6251  reuop  6252  iota5  6476  funopg  6527  fneq2  6585  foeq3  6745  tz6.12f  6860  funbrfv  6883  fnbrfvb  6885  fvelimab  6907  elrnrexdm  7036  funsndifnop  7099  fconst5  7155  eufnfv  7178  f1veqaeq  7205  fpropnf1  7216  nf1const  7253  isosolem  7296  f1opr  7417  mpoeq123  7433  ovmpt4g  7508  ov3  7524  ovg  7526  caovcang  7562  caovcan  7565  tfisi  7804  tfindsg  7806  findsg  7842  f1oweALT  7919  seqomlem2  8384  oawordeu  8484  omopth  8592  ereq2  8646  qsdisj  8735  eroveu  8753  2dom  8971  fundmen  8972  xpf1o  9071  nneneq  9134  pwfir  9221  cantnflem1  9604  brttrcl  9628  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  updjud  9852  alephfp  10024  dfac5  10045  cardcf  10168  cfeq0  10172  sornom  10193  fpwwe2cbv  10547  fpwwe2lem3  10550  ltsosr  11011  map2psrpr  11027  axpre-lttri  11082  subval  11378  divval  11805  nn0ind-raph  12623  fvf1tp  13742  uzrdgfni  13914  sqeqor  14172  nn0opth2  14228  hashrabsn1  14330  elprchashprn2  14352  hashbclem  14408  hashbc  14409  hash2prde  14426  hash2pwpr  14432  brfi1indALT  14466  wrdind  14678  wrd2ind  14679  reuccatpfxs1lem  14702  cshf1  14766  wrdl3s3  14918  relexpindlem  15019  sqrtval  15193  sqrmo  15207  reusq0  15421  summolem2  15672  prodmolem2  15894  divides  16217  dvdstr  16257  odd2np1lem  16303  ndvdssub  16372  bitsinv1  16405  eucalglt  16548  hashgcdeq  16754  ramcl2lem  16974  ramcl  16994  cshwrepswhash1  17067  imasaddfnlem  17486  fnhomeqhomf  17651  initoeu2lem1  17975  cat1lem  18057  posi  18277  sgrp2nmndlem3  18890  dfgrp2  18932  grpidinv  18968  dfgrp3lem  19008  orbsta  19282  symgfvne  19350  symgfix2  19385  odlem1  19504  gexlem1  19548  slwispgp  19580  sylow3lem6  19601  efgrelexlemb  19719  gsumval3lem2  19875  pgpfac1  20051  pgpfaclem2  20053  pgpfac  20055  ablfaclem1  20056  isdomn  20676  isdomn4  20687  domnlcanb  20691  domnrcanb  20693  obsip  21714  uvcval  21778  mvrval  21973  mhpval  22118  psdfval  22137  psdmvr  22148  coe1tmmul2  22254  coe1tmmul  22255  mat1comp  22418  mat1dimid  22452  scmateALT  22490  marrepval  22540  marepvval  22545  minmar1val  22626  gsummatr01  22637  t0sep  23302  t1sep2  23347  is2ndc  23424  kqt0lem  23714  isr0  23715  isufil2  23886  xmeteq0  24316  imasf1oxmet  24353  xrsxmet  24788  iccpnfcnv  24924  dyadmax  25578  dyadmbl  25580  dvfsumle  26001  dvfsumabs  26003  dvfsumlem1  26006  mdegle0  26055  fta1g  26148  ig1peu  26153  fta1  26288  aalioulem2  26313  taylthlem2  26354  efopn  26638  efrlim  26949  efrlimOLD  26950  musum  27171  mpodvdsmulf1o  27174  dvdsmulf1o  27176  dchrsum2  27248  sumdchr2  27250  gausslemma2dlem0i  27344  addsqnreup  27423  2sqreulem1  27426  2sqreultblem  27428  2sqreunnlem1  27429  2sqreunnltblem  27431  2sqreulem3  27433  ltsres  27643  nosupprefixmo  27681  noinfprefixmo  27682  nosupcbv  27683  nosupno  27684  nosupfv  27687  noinfcbv  27698  noinfno  27699  noinffv  27702  elmade  27866  divsval  28198  noseqrdgfn  28315  bdayn0sf1o  28379  bdayfinbndlem2  28477  axtgcgrid  28548  axtgbtwnid  28551  tglowdim1i  28586  islmib  28872  axcontlem12  29061  upgredgpr  29228  ushgredgedg  29315  ushgredgedgloop  29317  rusgrpropnb  29670  rgrx0ndm  29680  uspgr2wlkeq  29732  wlkson  29741  upgrwlkdvdelem  29822  spthonepeq  29838  iswwlksnon  29939  wlklnwwlkln2lem  29968  wwlksnredwwlkn  29981  wwlksnextprop  29998  wwlksnwwlksnon  30001  elwwlks2ons3  30041  rusgrnumwwlklem  30059  clwlkclwwlklem2a4  30085  clwwlkn  30114  clwwlkext2edg  30144  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknon  30178  clwwlk0on0  30180  uhgr3cyclexlem  30269  1conngr  30282  frgr3vlem1  30361  3vfriswmgrlem  30365  frgrwopreglem3  30402  fusgreg2wsplem  30421  fusgreghash2wsp  30426  numclwlk1lem1  30457  numclwwlkovq  30462  numclwwlk2lem1  30464  frgrregord013  30483  friendshipgt3  30486  ex-opab  30520  isgrpoi  30587  grpoidinv2  30604  hvsubeq0  31157  hvaddcan  31159  hvsubadd  31166  normsub0  31225  omlsi  31493  pjoml  31525  nonbooli  31740  pj11  31803  lnopeq  32098  nmopun  32103  pjclem4a  32287  pj3lem1  32295  strlem4  32343  hstrlem4  32351  jplem1  32357  superpos  32443  ifeqeqx  32630  disji2f  32665  disjif2  32669  disjabrex  32670  disjabrexf  32671  disjxpin  32676  disjunsn  32682  ofpreima  32756  fgreu  32762  fcnvgreu  32763  sgnsub  32928  gsumhashmul  33146  elrgspnlem2  33322  elrgspnlem3  33323  elrgspnlem4  33324  domnlcanOLD  33359  ismxidl  33540  mplmulmvr  33701  psrmonmul2  33713  esplyfval  33725  esplyfval0  33726  esplyfv  33732  esplyfval3  33734  esplyfvaln  33736  xrge0iifcnv  34096  esumpr2  34230  eulerpartlemgvv  34539  eulerpartlemgh  34541  eulerpartlemgs2  34543  plymulx0  34710  lpadmax  34845  lpadright  34847  bnj1321  35188  f1resfz0f1d  35315  subfacp1lem3  35383  pconncn  35425  cnpconn  35431  txpconn  35433  connpconn  35436  cvmlift3lem2  35521  cvmlift3lem4  35523  cvmlift3  35529  snmlflim  35533  iota5f  35925  rankeq1o  36372  nn0prpw  36524  tr0elw  36685  tr0el  36686  dfttc4lem1  36729  elttcirr  36732  bj-csbsnlem  37229  bj-elgab  37265  bj-restsnss  37414  bj-restsnss2  37415  bj-imdirco  37523  wl-isseteq  37838  wl-ax12v2cl  37839  wl-dfcleq  37847  fin2so  37945  poimirlem2  37960  poimirlem18  37976  poimirlem21  37979  poimirlem25  37983  poimirlem26  37984  poimirlem27  37985  mblfinlem2  37996  mbfresfi  38004  cnambfre  38006  ftc1anclem8  38038  fdc  38083  istotbnd  38107  isexid2  38193  isgrpda  38293  ismaxidl  38378  mpobi123f  38500  mptbi12f  38504  disjressuc2  38749  qsdisjALTV  39037  parteq2  39216  lsatcmp  39466  lshpkrlem1  39573  trlval2  40626  cdlemg1cex  41051  cdlemm10N  41581  dicval  41639  lcmineqlem4  42488  grpods  42650  unitscyglem2  42652  unitscyglem3  42653  unitscyglem4  42654  exfinfldd  42659  nnn1suc  42721  resubval  42816  redivvald  42891  fsuppind  43040  unxpwdom3  43544  dgraalem  43594  dgraaub  43597  onsucf1lem  43718  frege104  44415  pm13.192  44858  2sbc6g  44863  2sbc5g  44864  pm14.122b  44871  equncomVD  45315  csbingVD  45331  csbsngVD  45340  csbxpgVD  45341  csbresgVD  45342  csbrngVD  45343  csbima12gALTVD  45344  csbunigVD  45345  csbfv12gALTVD  45346  relopabVD  45348  dvnprodlem1  46395  dvnprodlem2  46396  dvnprodlem3  46397  dvnprod  46398  fourierdlem42  46598  etransclem11  46694  etransclem12  46695  etransclem33  46716  nnfoctbdjlem  46904  hoimbl  47080  cfsetsnfsetf  47521  aiota0def  47559  euoreqb  47572  funressndmafv2rn  47686  funressnbrafv2  47707  dfatbrafv2b  47708  funbrafv2  47710  fnbrafv2b  47711  elsetpreimafvbi  47866  elsetpreimafveq  47872  imasetpreimafvbijlemfo  47880  fargshiftf1  47916  ichnreuop  47947  paireqne  47986  reupr  47997  isuspgrim0  48385  upgrimpths  48400  clnbgrgrim  48425  grimedg  48426  isubgr3stgrlem4  48460  isubgr3stgrlem7  48463  gpgedg2ov  48557  gpgedg2iv  48558  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem4  48610  pgnbgreunbgr  48616  uspgrsprf1  48638  uspgrsprfo  48639  lidldomn1  48722  nn0sumshdiglem2  49113  mof0  49328  eufsnlem  49331  oppcmndclem  49507  isthincd2lem1  49915  termcbasmo  49973  termcarweu  50018  arweuthinc  50019  arweutermc  50020  setrec2lem2  50184