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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqeq12i  2781  eqtri  2786  neeq2i  3024  rabid2f  3446  rabid2im  3447  abv  3466  equncom  4161  eq0  4300  ab0w  4331  ab0  4332  ab0orv  4335  absn  4604  rabrsn  4687  ssunpr  4794  sspr  4795  sstp  4796  preq12b  4810  preqsnd  4819  preq12nebg  4823  opthprneg  4825  opeqpr  5484  propssopi  5487  wefrc  5652  el2xptp  5830  dfrel4v  6200  dfrel4  6201  cnveq0  6209  orddif  6487  funopg  6602  funcocnv2OLD  6881  dffn5f  6987  fnressn  7194  fressnfv  7196  fnprb  7245  fntpb  7246  riotaeqimp  7434  fnov  7582  ovmpos  7600  onuninsuci  7885  fvresex  8006  elxp6  8069  el2xptp0  8081  opiota  8105  tpossym  8313  qsid  8840  mapsncnv  8959  ixpsnf1o  9004  card1  10086  pm54.43lem  10120  cf0  10367  sdom2en01  10419  cardeq0  10675  enqbreq2  11044  addcompr  11145  mulcompr  11147  axrrecex  11287  negeq0  11651  muleqadd  12000  crne0  12353  dfnn3  12389  xmulneg1  13439  hasheq0  14548  hashbc  14639  hashf1lem2  14642  hash2pwpr  14662  eqwrds3  15157  cjne0  15373  sqrt00  15473  sqrtmsq2i  15599  cbvsum  15906  cbvsumv  15907  fsump1i  15979  cbvprod  16126  cbvprodv  16127  bpoly2  16267  bpoly3  16268  bpoly4  16269  absefib  16410  efieq1re  16411  xpccatid  18412  sgrpidmnd  18978  smndex2dnrinv  19164  isnsg4  19427  opprdomnb  21019  selvval  22484  mat1dimelbas  22841  matunitlindflem1  23049  pmatcollpw3fi1lem1  23159  2ndcctbss  23829  ptcnp  23996  ovolgelb  25856  ioorinv  25952  dvcobr  26321  rolle  26365  dvfsumlem2  26402  plymul0or  26654  reeff1o  26831  sineq0  26909  coseq1  26910  1cubr  27227  atandm2  27262  atandm3  27263  efrlim  27354  isppw  27498  ppiub  27588  lgsdinn0  27729  m1lgs  27772  elzs2  28842  elznns  28845  twocut  28866  uhgr2edg  29846  usgredg2vlem1  29863  usgredg2vlem2  29864  ushgredgedg  29867  ushgredgedgloop  29869  edgnbusgreu  30005  nb3grprlem2  30019  nb3gr2nb  30022  usgredgsscusgredg  30097  usgr2wlkneq  30399  usgr2pthlem  30406  crctcshwlkn0  30467  wwlksn0s  30507  umgr2adedgwlk  30591  umgr2adedgspth  30594  elwwlks2s3  30597  elwwlks2ons3im  30600  rusgrnumwwlkl1  30617  clwlkclwwlkflem  30652  isfrgr  30918  frgr3v  30933  frgrregorufr0  30982  isgrpo  31156  vciOLD  31220  chnlei  32144  h1de2ctlem  32214  cmcmlem  32250  cmcm2i  32252  cmbr2i  32255  osumcor2i  32303  pjss2i  32339  ho01i  32487  nmop0h  32650  pjclem1  32854  jplem1  32927  atabs2i  33061  1arithidom  34173  ply1dg1rt  34215  selvply1rhmlem2  34264  esplyfval1  34316  vieta  34323  fedgmullem2  34373  ccfldextdgrr  34415  zarcls  34617  breprexp  35373  bnj168  35472  bnj927  35511  bnj543  35634  bnj970  35688  dfj2  36050  subfacp1lem6  36158  satfv1  36336  satfvsucsuc  36338  satf0  36345  fmlaomn0  36363  fmla0disjsuc  36371  satffunlem2lem1  36377  mppspstlem  36544  quad3  36643  brdomain  36910  brrange  36911  brimg  36914  brapply  36915  lemsuccf  36918  brfullfun  36927  brrestrict  36928  rankeq1o  37147  sumeq2si  37206  prodeq2si  37208  cbvprodvw2  37251  bj-snsetex  38091  bj-reabeq  38155  bj-rest10  38279  bj-ismooredr2  38301  bj-pinftynminfty  38416  dffinxpf  38576  finxp0  38582  ismblfin  38847  opropabco  38926  fdc  38945  isdrngo1  39156  smprngopr  39252  qseq  39931  eldisjlem19  40111  cdleme25cv  41681  cdlemk35  42235  dicval2  42502  dicopelval2  42504  dicelval2N  42505  hdmap1fval  43119  sn-0tie0  43781  absnw  43955  mzpcompact2lem  44028  eldioph4b  44084  2nn0ind  44218  islmodfg  44337  abeqabi  44670  relintab  44845  brtrclfv2  44988  frege116  45240  elnev  45681  dvnprodlem1  47229  fourierdlem103  47492  fourierdlem104  47493  ovnovollem3  47941  aiotaexim  48441  fmtno4prmfac  48930  usgrexmpl2nb1  49403  usgrexmpl2nb2  49404  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  pgnioedg1  49479  pgnioedg2  49480  pgnioedg3  49481  pgnioedg4  49482  pgnioedg5  49483  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  pgnbgreunbgrlem5lem1  49491  pgnbgreunbgrlem5lem2  49492  pgnbgreunbgrlem5lem3  49493  smprngprmrng  49767  lindsrng01  49911  ldepspr  49916  nn0sumshdiglemB  50063  mofeu  50290  f1omo  50338  veronesevrowd  51407