Theorem eqeq2i 2749

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eqeq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq2i	⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq2 2748	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728

This theorem is referenced by:  eqeq12i  2754  eqtri  2764  neeq2i  3007  rabid2f  3325  rabid2OLD  3327  abv  3448  dfss2OLD  3913  equncom  4094  eq0  4283  ab0w  4313  ab0  4314  ab0OLD  4315  ab0orv  4318  eq0rdv  4344  rzal  4445  absn  4583  rabrsn  4664  ssunpr  4771  sspr  4772  sstp  4773  preq12b  4787  preqsnd  4795  preq12nebg  4799  opthprneg  4801  opeqpr  5432  propssopi  5435  wefrc  5594  dfrel4v  6108  dfrel4  6109  orddif  6376  funopg  6497  funimaexgOLD  6550  funcocnv2  6771  dffn5f  6872  fnressn  7062  fressnfv  7064  fnprb  7116  fntpb  7117  riotaeqimp  7291  fnov  7437  ovmpos  7453  onuninsuci  7719  fvresex  7834  elxp6  7897  el2xptp  7909  el2xptp0  7910  opiota  7931  tpossym  8105  dfwrecsOLD  8160  qsid  8603  mapsncnv  8712  ixpsnf1o  8757  card1  9770  pm54.43lem  9802  cf0  10053  sdom2en01  10104  cardeq0  10354  enqbreq2  10722  addcompr  10823  mulcompr  10825  axrrecex  10965  negeq0  11321  muleqadd  11665  crne0  12012  dfnn3  12033  xmulneg1  13049  hasheq0  14123  hashbc  14210  hashf1lem2  14215  hash2pwpr  14235  eqwrds3  14721  cjne0  14919  sqrt00  15020  sqrtmsq2i  15144  cbvsum  15452  fsump1i  15526  cbvprod  15670  bpoly2  15812  bpoly3  15813  bpoly4  15814  absefib  15952  efieq1re  15953  xpccatid  17950  sgrpidmnd  18435  smndex2dnrinv  18599  isnsg4  18840  selvval  21373  mat1dimelbas  21665  pmatcollpw3fi1lem1  21980  2ndcctbss  22651  ptcnp  22818  ovolgelb  24689  ioorinv  24785  rolle  25199  plymul0or  25486  reeff1o  25651  sineq0  25725  coseq1  25726  1cubr  26037  atandm2  26072  atandm3  26073  efrlim  26164  isppw  26308  ppiub  26397  lgsdinn0  26538  m1lgs  26581  uhgr2edg  27620  usgredg2vlem1  27637  usgredg2vlem2  27638  ushgredgedg  27641  ushgredgedgloop  27643  edgnbusgreu  27779  nb3grprlem2  27793  nb3gr2nb  27796  usgredgsscusgredg  27871  usgr2wlkneq  28169  usgr2pthlem  28176  crctcshwlkn0  28231  wwlksn0s  28271  umgr2adedgwlk  28355  umgr2adedgspth  28358  elwwlks2s3  28361  elwwlks2ons3im  28364  rusgrnumwwlkl1  28378  clwlkclwwlkflem  28413  isfrgr  28669  frgr3v  28684  frgrregorufr0  28733  isgrpo  28904  vciOLD  28968  chnlei  29892  h1de2ctlem  29962  cmcmlem  29998  cmcm2i  30000  cmbr2i  30003  osumcor2i  30051  pjss2i  30087  ho01i  30235  nmop0h  30398  pjclem1  30602  jplem1  30675  atabs2i  30809  fedgmullem2  31756  ccfldextdgrr  31787  zarcls  31869  breprexp  32658  bnj168  32754  bnj927  32794  bnj543  32918  bnj970  32972  subfacp1lem6  33192  satfv1  33370  satfvsucsuc  33372  satf0  33379  fmlaomn0  33397  fmla0disjsuc  33405  satffunlem2lem1  33411  mppspstlem  33578  quad3  33673  brdomain  34280  brrange  34281  brimg  34284  brapply  34285  brsuccf  34288  brfullfun  34295  brrestrict  34296  rankeq1o  34518  bj-snsetex  35197  bj-reabeq  35261  bj-rest10  35303  bj-ismooredr2  35325  bj-pinftynminfty  35442  dffinxpf  35600  finxp0  35606  matunitlindflem1  35817  ismblfin  35862  opropabco  35926  fdc  35947  isdrngo1  36158  smprngopr  36254  cdleme25cv  38414  cdlemk35  38968  dicval2  39235  dicopelval2  39237  dicelval2N  39238  hdmap1fval  39852  sn-0tie0  40458  mzpcompact2lem  40610  eldioph4b  40670  2nn0ind  40805  islmodfg  40932  relintab  41229  brtrclfv2  41373  frege116  41625  elnev  42094  dvnprodlem1  43536  fourierdlem103  43799  fourierdlem104  43800  ovnovollem3  44246  fmtno4prmfac  45082  lindsrng01  45867  ldepspr  45872  nn0sumshdiglemB  46024  mofeu  46233