Theorem eqeq2 2752

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqeq2i  2753  eqeq12OLD  2759  eqtr3  2766  clelab  2890  alexeqg  3664  pm13.183  3679  elab6g  3682  eqeu  3728  moeq3  3734  mo2icl  3736  mob2  3737  euind  3746  reu6i  3750  reu2eqd  3758  reuind  3775  sbc2or  3813  sbc5ALT  3833  csbiebg  3954  eqif  4589  sneq  4658  reusngf  4696  rexreusng  4703  reuprg0  4727  preq1b  4871  preq12bg  4878  preqsn  4886  disji2  5150  disjprg  5162  dtruALT  5406  opth  5496  euotd  5532  solin  5634  ideqg  5876  resieq  6020  cnveqb  6227  cnveq0  6228  reu3op  6323  reuop  6324  iota5  6556  funopg  6612  fneq2  6671  foeq3  6832  tz6.12f  6946  funbrfv  6971  fnbrfvb  6973  fvelimab  6994  elrnrexdm  7123  funsndifnop  7185  fconst5  7243  eufnfv  7266  f1veqaeq  7294  fpropnf1  7304  nf1const  7340  isosolem  7383  f1opr  7506  mpoeq123  7522  ovmpt4g  7597  ov3  7613  ovg  7615  caovcang  7651  caovcan  7654  tfisi  7896  tfindsg  7898  findsg  7937  f1oweALT  8013  seqomlem2  8507  oawordeu  8611  omopth  8718  ereq2  8771  qsdisj  8852  eroveu  8870  2dom  9095  fundmen  9096  xpf1o  9205  nneneq  9272  nneneqOLD  9284  pwfir  9383  cantnflem1  9758  brttrcl  9782  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  updjud  10003  alephfp  10177  dfac5  10198  cardcf  10321  cfeq0  10325  sornom  10346  fpwwe2cbv  10699  fpwwe2lem3  10702  ltsosr  11163  map2psrpr  11179  axpre-lttri  11234  subval  11527  divval  11951  nn0ind-raph  12743  fvf1tp  13840  uzrdgfni  14009  sqeqor  14265  nn0opth2  14321  hashrabsn1  14423  elprchashprn2  14445  hashbclem  14501  hashbc  14502  hash2prde  14519  hash2pwpr  14525  brfi1indALT  14559  wrdind  14770  wrd2ind  14771  reuccatpfxs1lem  14794  cshf1  14858  wrdl3s3  15011  relexpindlem  15112  sqrtval  15286  sqrmo  15300  reusq0  15511  summolem2  15764  prodmolem2  15983  divides  16304  dvdstr  16342  odd2np1lem  16388  ndvdssub  16457  bitsinv1  16488  eucalglt  16632  hashgcdeq  16836  ramcl2lem  17056  ramcl  17076  cshwrepswhash1  17150  imasaddfnlem  17588  fnhomeqhomf  17749  initoeu2lem1  18081  cat1lem  18163  posi  18387  sgrp2nmndlem3  18960  dfgrp2  19002  grpidinv  19038  dfgrp3lem  19078  orbsta  19353  symgfvne  19422  symgfix2  19458  odlem1  19577  gexlem1  19621  slwispgp  19653  sylow3lem6  19674  efgrelexlemb  19792  gsumval3lem2  19948  pgpfac1  20124  pgpfaclem2  20126  pgpfac  20128  ablfaclem1  20129  isdomn  20727  isdomn4  20738  domnlcanb  20742  domnrcanb  20744  obsip  21764  uvcval  21828  mvrval  22025  mhpval  22166  psdfval  22185  coe1tmmul2  22300  coe1tmmul  22301  mat1comp  22467  mat1dimid  22501  scmateALT  22539  marrepval  22589  marepvval  22594  minmar1val  22675  gsummatr01  22686  t0sep  23353  t1sep2  23398  is2ndc  23475  kqt0lem  23765  isr0  23766  isufil2  23937  xmeteq0  24369  imasf1oxmet  24406  xrsxmet  24850  iccpnfcnv  24994  dyadmax  25652  dyadmbl  25654  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem1  26086  mdegle0  26136  fta1g  26229  ig1peu  26234  fta1  26368  aalioulem2  26393  taylthlem2  26434  efopn  26718  efrlim  27030  efrlimOLD  27031  musum  27252  mpodvdsmulf1o  27255  dvdsmulf1o  27257  dchrsum2  27330  sumdchr2  27332  gausslemma2dlem0i  27426  addsqnreup  27505  2sqreulem1  27508  2sqreultblem  27510  2sqreunnlem1  27511  2sqreunnltblem  27513  2sqreulem3  27515  sltres  27725  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupno  27766  nosupfv  27769  noinfcbv  27780  noinfno  27781  noinffv  27784  elmade  27924  divsval  28233  noseqrdgfn  28330  axtgcgrid  28489  axtgbtwnid  28492  tglowdim1i  28527  islmib  28813  axcontlem12  29008  upgredgpr  29177  ushgredgedg  29264  ushgredgedgloop  29266  rusgrpropnb  29619  rgrx0ndm  29629  uspgr2wlkeq  29682  wlkson  29692  upgrwlkdvdelem  29772  spthonepeq  29788  iswwlksnon  29886  wlklnwwlkln2lem  29915  wwlksnredwwlkn  29928  wwlksnextprop  29945  wwlksnwwlksnon  29948  elwwlks2ons3  29988  rusgrnumwwlklem  30003  clwlkclwwlklem2a4  30029  clwwlkn  30058  clwwlkext2edg  30088  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwwlknon  30122  clwwlk0on0  30124  uhgr3cyclexlem  30213  1conngr  30226  frgr3vlem1  30305  3vfriswmgrlem  30309  frgrwopreglem3  30346  fusgreg2wsplem  30365  fusgreghash2wsp  30370  numclwlk1lem1  30401  numclwwlkovq  30406  numclwwlk2lem1  30408  frgrregord013  30427  friendshipgt3  30430  ex-opab  30464  isgrpoi  30530  grpoidinv2  30547  hvsubeq0  31100  hvaddcan  31102  hvsubadd  31109  normsub0  31168  omlsi  31436  pjoml  31468  nonbooli  31683  pj11  31746  lnopeq  32041  nmopun  32046  pjclem4a  32230  pj3lem1  32238  strlem4  32286  hstrlem4  32294  jplem1  32300  superpos  32386  ifeqeqx  32565  disji2f  32599  disjif2  32603  disjabrex  32604  disjabrexf  32605  disjxpin  32610  disjunsn  32616  ofpreima  32683  fgreu  32690  fcnvgreu  32691  gsumhashmul  33040  domnlcanOLD  33249  ismxidl  33455  xrge0iifcnv  33879  esumpr2  34031  eulerpartlemgvv  34341  eulerpartlemgh  34343  eulerpartlemgs2  34345  sgnsub  34509  plymulx0  34524  lpadmax  34659  lpadright  34661  bnj1321  35003  f1resfz0f1d  35081  subfacp1lem3  35150  pconncn  35192  cnpconn  35198  txpconn  35200  connpconn  35203  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3  35296  snmlflim  35300  iota5f  35686  rankeq1o  36135  nn0prpw  36289  bj-csbsnlem  36869  bj-elgab  36905  bj-restsnss  37049  bj-restsnss2  37050  bj-imdirco  37156  fin2so  37567  poimirlem2  37582  poimirlem18  37598  poimirlem21  37601  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  mblfinlem2  37618  mbfresfi  37626  cnambfre  37628  ftc1anclem8  37660  fdc  37705  istotbnd  37729  isexid2  37815  isgrpda  37915  ismaxidl  38000  mpobi123f  38122  mptbi12f  38126  disjressuc2  38344  qsdisjALTV  38571  parteq2  38731  lsatcmp  38959  lshpkrlem1  39066  trlval2  40120  cdlemg1cex  40545  cdlemm10N  41075  dicval  41133  lcmineqlem4  41989  grpods  42151  unitscyglem2  42153  unitscyglem3  42154  unitscyglem4  42155  exfinfldd  42160  nnn1suc  42255  resubval  42343  fsuppind  42545  unxpwdom3  43052  dgraalem  43102  dgraaub  43105  onsucf1lem  43231  frege104  43929  pm13.192  44379  2sbc6g  44384  2sbc5g  44385  pm14.122b  44392  equncomVD  44839  csbingVD  44855  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbima12gALTVD  44868  csbunigVD  44869  csbfv12gALTVD  44870  relopabVD  44872  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  dvnprod  45870  fourierdlem42  46070  etransclem11  46166  etransclem12  46167  etransclem33  46188  nnfoctbdjlem  46376  hoimbl  46552  cfsetsnfsetf  46973  aiota0def  47011  euoreqb  47024  funressndmafv2rn  47138  funressnbrafv2  47159  dfatbrafv2b  47160  funbrafv2  47162  fnbrafv2b  47163  elsetpreimafvbi  47265  elsetpreimafveq  47271  imasetpreimafvbijlemfo  47279  fargshiftf1  47315  ichnreuop  47346  paireqne  47385  reupr  47396  isuspgrim0  47756  clnbgrgrim  47786  grimedg  47787  uspgrsprf1  47870  uspgrsprfo  47871  lidldomn1  47954  nn0sumshdiglem2  48356  mof0  48551  eufsnlem  48554  isthincd2lem1  48694  setrec2lem2  48786