Theorem eqeq2i 2752

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 2751	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731

This theorem is referenced by:  eqeq12i  2757  eqtri  2767  neeq2i  3010  rabid2f  3311  rabid2OLD  3313  abv  3441  dfss2OLD  3912  equncom  4092  eq0  4282  ab0w  4312  ab0  4313  ab0OLD  4314  ab0orv  4317  eq0rdv  4343  rzal  4444  absn  4584  rabrsn  4665  ssunpr  4770  sspr  4771  sstp  4772  preq12b  4786  preqsnd  4794  preq12nebg  4798  opthprneg  4800  opeqpr  5421  propssopi  5424  wefrc  5582  dfrel4v  6090  dfrel4  6091  orddif  6356  funopg  6464  funimaexg  6516  funcocnv2  6736  dffn5f  6834  fnressn  7024  fressnfv  7026  fnprb  7078  fntpb  7079  riotaeqimp  7252  fnov  7396  ovmpos  7412  onuninsuci  7675  fvresex  7789  elxp6  7851  el2xptp  7863  el2xptp0  7864  opiota  7885  tpossym  8058  dfwrecsOLD  8113  qsid  8546  mapsncnv  8655  ixpsnf1o  8700  trpredmintr  9461  card1  9710  pm54.43lem  9742  cf0  9991  sdom2en01  10042  cardeq0  10292  enqbreq2  10660  addcompr  10761  mulcompr  10763  axrrecex  10903  negeq0  11258  muleqadd  11602  crne0  11949  dfnn3  11970  xmulneg1  12985  hasheq0  14059  hashbc  14146  hashf1lem2  14151  hash2pwpr  14171  eqwrds3  14657  cjne0  14855  sqrt00  14956  sqrtmsq2i  15080  cbvsum  15388  fsump1i  15462  cbvprod  15606  bpoly2  15748  bpoly3  15749  bpoly4  15750  absefib  15888  efieq1re  15889  xpccatid  17886  sgrpidmnd  18371  smndex2dnrinv  18535  isnsg4  18776  selvval  21309  mat1dimelbas  21601  pmatcollpw3fi1lem1  21916  2ndcctbss  22587  ptcnp  22754  ovolgelb  24625  ioorinv  24721  rolle  25135  plymul0or  25422  reeff1o  25587  sineq0  25661  coseq1  25662  1cubr  25973  atandm2  26008  atandm3  26009  efrlim  26100  isppw  26244  ppiub  26333  lgsdinn0  26474  m1lgs  26517  uhgr2edg  27556  usgredg2vlem1  27573  usgredg2vlem2  27574  ushgredgedg  27577  ushgredgedgloop  27579  edgnbusgreu  27715  nb3grprlem2  27729  nb3gr2nb  27732  usgredgsscusgredg  27807  usgr2wlkneq  28103  usgr2pthlem  28110  crctcshwlkn0  28165  wwlksn0s  28205  umgr2adedgwlk  28289  umgr2adedgspth  28292  elwwlks2s3  28295  elwwlks2ons3im  28298  rusgrnumwwlkl1  28312  clwlkclwwlkflem  28347  isfrgr  28603  frgr3v  28618  frgrregorufr0  28667  isgrpo  28838  vciOLD  28902  chnlei  29826  h1de2ctlem  29896  cmcmlem  29932  cmcm2i  29934  cmbr2i  29937  osumcor2i  29985  pjss2i  30021  ho01i  30169  nmop0h  30332  pjclem1  30536  jplem1  30609  atabs2i  30743  fedgmullem2  31690  ccfldextdgrr  31721  zarcls  31803  breprexp  32592  bnj168  32688  bnj927  32728  bnj543  32852  bnj970  32906  subfacp1lem6  33126  satfv1  33304  satfvsucsuc  33306  satf0  33313  fmlaomn0  33331  fmla0disjsuc  33339  satffunlem2lem1  33345  mppspstlem  33512  quad3  33607  brdomain  34214  brrange  34215  brimg  34218  brapply  34219  brsuccf  34222  brfullfun  34229  brrestrict  34230  rankeq1o  34452  bj-snsetex  35132  bj-reabeq  35196  bj-rest10  35238  bj-ismooredr2  35260  bj-pinftynminfty  35377  dffinxpf  35535  finxp0  35541  matunitlindflem1  35752  ismblfin  35797  opropabco  35861  fdc  35882  isdrngo1  36093  smprngopr  36189  cdleme25cv  38351  cdlemk35  38905  dicval2  39172  dicopelval2  39174  dicelval2N  39175  hdmap1fval  39789  sn-0tie0  40401  mzpcompact2lem  40553  eldioph4b  40613  2nn0ind  40747  islmodfg  40874  relintab  41144  brtrclfv2  41288  frege116  41540  elnev  42009  dvnprodlem1  43441  fourierdlem103  43704  fourierdlem104  43705  ovnovollem3  44150  fmtno4prmfac  44976  lindsrng01  45761  ldepspr  45766  nn0sumshdiglemB  45918  mofeu  46127