Theorem eqeq2i 2776

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755

This theorem is used by:  eqeq12i  2781  eqtri  2786  neeq2i  3023  rabid2f  3445  rabid2im  3446  abv  3465  equncom  4160  eq0  4299  ab0w  4330  ab0  4331  ab0orv  4334  absn  4603  rabrsn  4684  ssunpr  4791  sspr  4792  sstp  4793  preq12b  4807  preqsnd  4816  preq12nebg  4820  opthprneg  4822  opeqpr  5480  propssopi  5483  wefrc  5648  el2xptp  5824  dfrel4v  6187  dfrel4  6188  cnveq0  6196  orddif  6467  funopg  6582  funcocnv2  6858  dffn5f  6964  fnressn  7170  fressnfv  7172  fnprb  7221  fntpb  7222  riotaeqimp  7410  fnov  7558  ovmpos  7575  onuninsuci  7858  fvresex  7979  elxp6  8042  el2xptp0  8054  opiota  8078  tpossym  8286  qsid  8813  mapsncnv  8932  ixpsnf1o  8977  card1  10059  pm54.43lem  10091  cf0  10338  sdom2en01  10390  cardeq0  10646  enqbreq2  11015  addcompr  11116  mulcompr  11118  axrrecex  11258  negeq0  11622  muleqadd  11970  crne0  12323  dfnn3  12359  xmulneg1  13409  hasheq0  14517  hashbc  14608  hashf1lem2  14611  hash2pwpr  14631  eqwrds3  15126  cjne0  15342  sqrt00  15442  sqrtmsq2i  15567  cbvsum  15874  cbvsumv  15875  fsump1i  15947  cbvprod  16094  cbvprodv  16095  bpoly2  16235  bpoly3  16236  bpoly4  16237  absefib  16378  efieq1re  16379  xpccatid  18374  sgrpidmnd  18940  smndex2dnrinv  19126  isnsg4  19389  opprdomnb  20980  selvval  22441  mat1dimelbas  22798  matunitlindflem1  23006  pmatcollpw3fi1lem1  23116  2ndcctbss  23786  ptcnp  23953  ovolgelb  25813  ioorinv  25909  dvcobr  26278  rolle  26322  dvfsumlem2  26359  plymul0or  26611  reeff1o  26786  sineq0  26864  coseq1  26865  1cubr  27182  atandm2  27217  atandm3  27218  efrlim  27309  isppw  27453  ppiub  27543  lgsdinn0  27684  m1lgs  27727  elzs2  28797  elznns  28800  twocut  28821  uhgr2edg  29801  usgredg2vlem1  29818  usgredg2vlem2  29819  ushgredgedg  29822  ushgredgedgloop  29824  edgnbusgreu  29960  nb3grprlem2  29974  nb3gr2nb  29977  usgredgsscusgredg  30052  usgr2wlkneq  30354  usgr2pthlem  30361  crctcshwlkn0  30422  wwlksn0s  30462  umgr2adedgwlk  30546  umgr2adedgspth  30549  elwwlks2s3  30552  elwwlks2ons3im  30555  rusgrnumwwlkl1  30572  clwlkclwwlkflem  30607  isfrgr  30873  frgr3v  30888  frgrregorufr0  30937  isgrpo  31111  vciOLD  31175  chnlei  32099  h1de2ctlem  32169  cmcmlem  32205  cmcm2i  32207  cmbr2i  32210  osumcor2i  32258  pjss2i  32294  ho01i  32442  nmop0h  32605  pjclem1  32809  jplem1  32882  atabs2i  33016  1arithidom  34122  ply1dg1rt  34165  selvply1rhmlem2  34206  esplyfval1  34258  vieta  34265  fedgmullem2  34315  ccfldextdgrr  34357  zarcls  34559  breprexp  35315  bnj168  35414  bnj927  35453  bnj543  35576  bnj970  35630  dfj2  35963  subfacp1lem6  36071  satfv1  36249  satfvsucsuc  36251  satf0  36258  fmlaomn0  36276  fmla0disjsuc  36284  satffunlem2lem1  36290  mppspstlem  36457  quad3  36556  brdomain  36822  brrange  36823  brimg  36826  brapply  36827  lemsuccf  36830  brfullfun  36839  brrestrict  36840  rankeq1o  37059  sumeq2si  37118  prodeq2si  37120  cbvprodvw2  37163  bj-snsetex  38003  bj-reabeq  38067  bj-rest10  38148  bj-ismooredr2  38170  bj-pinftynminfty  38288  dffinxpf  38448  finxp0  38454  ismblfin  38719  opropabco  38798  fdc  38819  isdrngo1  39030  smprngopr  39126  qseq  39805  eldisjlem19  39985  cdleme25cv  41555  cdlemk35  42109  dicval2  42376  dicopelval2  42378  dicelval2N  42379  hdmap1fval  42993  sn-0tie0  43655  absnw  43829  mzpcompact2lem  43902  eldioph4b  43958  2nn0ind  44092  islmodfg  44211  abeqabi  44549  relintab  44724  brtrclfv2  44867  frege116  45119  elnev  45560  dvnprodlem1  47095  fourierdlem103  47358  fourierdlem104  47359  ovnovollem3  47807  aiotaexim  48307  fmtno4prmfac  48796  usgrexmpl2nb1  49269  usgrexmpl2nb2  49270  usgrexmpl2nb3  49271  usgrexmpl2nb4  49272  usgrexmpl2nb5  49273  pgnioedg1  49345  pgnioedg2  49346  pgnioedg3  49347  pgnioedg4  49348  pgnioedg5  49349  pgnbgreunbgrlem2lem1  49351  pgnbgreunbgrlem2lem2  49352  pgnbgreunbgrlem2lem3  49353  pgnbgreunbgrlem5lem1  49357  pgnbgreunbgrlem5lem2  49358  pgnbgreunbgrlem5lem3  49359  smprngprmrng  49575  lindsrng01  49719  ldepspr  49724  nn0sumshdiglemB  49871  mofeu  50098  f1omo  50146  veronesevrowd  51193