Theorem eqeq2i 2774

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 2773	. 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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  eqeq12i  2779  eqtri  2784  neeq2i  3021  rabid2f  3443  rabid2im  3444  abv  3463  equncom  4106  eq0  4297  ab0w  4328  ab0  4329  ab0orv  4332  absn  4604  rabrsn  4685  ssunpr  4794  sspr  4795  sstp  4796  preq12b  4810  preqsnd  4819  preq12nebg  4823  opthprneg  4825  opeqpr  5477  propssopi  5480  wefrc  5645  el2xptp  5820  dfrel4v  6182  dfrel4  6183  orddif  6461  funopg  6574  funcocnv2  6850  dffn5f  6956  fnressn  7162  fressnfv  7164  fnprb  7214  fntpb  7215  riotaeqimp  7403  fnov  7551  ovmpos  7568  onuninsuci  7851  fvresex  7972  elxp6  8035  el2xptp0  8047  opiota  8070  tpossym  8275  qsid  8802  mapsncnv  8921  ixpsnf1o  8966  card1  10049  pm54.43lem  10081  cf0  10328  sdom2en01  10380  cardeq0  10636  enqbreq2  11005  addcompr  11106  mulcompr  11108  axrrecex  11248  negeq0  11612  muleqadd  11960  crne0  12313  dfnn3  12349  xmulneg1  13399  hasheq0  14507  hashbc  14598  hashf1lem2  14601  hash2pwpr  14621  eqwrds3  15114  cjne0  15330  sqrt00  15430  sqrtmsq2i  15555  cbvsum  15862  cbvsumv  15863  fsump1i  15935  cbvprod  16082  cbvprodv  16083  bpoly2  16223  bpoly3  16224  bpoly4  16225  absefib  16366  efieq1re  16367  xpccatid  18362  sgrpidmnd  18928  smndex2dnrinv  19114  isnsg4  19377  opprdomnb  20968  selvval  22429  mat1dimelbas  22786  matunitlindflem1  22994  pmatcollpw3fi1lem1  23104  2ndcctbss  23774  ptcnp  23941  ovolgelb  25801  ioorinv  25897  dvcobr  26266  rolle  26310  dvfsumlem2  26347  plymul0or  26599  reeff1o  26774  sineq0  26852  coseq1  26853  1cubr  27170  atandm2  27205  atandm3  27206  efrlim  27297  isppw  27441  ppiub  27531  lgsdinn0  27672  m1lgs  27715  elzs2  28785  elznns  28788  twocut  28809  uhgr2edg  29789  usgredg2vlem1  29806  usgredg2vlem2  29807  ushgredgedg  29810  ushgredgedgloop  29812  edgnbusgreu  29948  nb3grprlem2  29962  nb3gr2nb  29965  usgredgsscusgredg  30040  usgr2wlkneq  30342  usgr2pthlem  30349  crctcshwlkn0  30410  wwlksn0s  30450  umgr2adedgwlk  30534  umgr2adedgspth  30537  elwwlks2s3  30540  elwwlks2ons3im  30543  rusgrnumwwlkl1  30560  clwlkclwwlkflem  30595  isfrgr  30861  frgr3v  30876  frgrregorufr0  30925  isgrpo  31099  vciOLD  31163  chnlei  32087  h1de2ctlem  32157  cmcmlem  32193  cmcm2i  32195  cmbr2i  32198  osumcor2i  32246  pjss2i  32282  ho01i  32430  nmop0h  32593  pjclem1  32797  jplem1  32870  atabs2i  33004  1arithidom  34069  ply1dg1rt  34112  selvply1rhmlem2  34153  esplyfval1  34205  vieta  34212  fedgmullem2  34262  ccfldextdgrr  34304  zarcls  34506  breprexp  35262  bnj168  35361  bnj927  35400  bnj543  35523  bnj970  35577  subfacp1lem6  35950  satfv1  36128  satfvsucsuc  36130  satf0  36137  fmlaomn0  36155  fmla0disjsuc  36163  satffunlem2lem1  36169  mppspstlem  36336  quad3  36435  brdomain  36695  brrange  36696  brimg  36699  brapply  36700  lemsuccf  36703  brfullfun  36712  brrestrict  36713  rankeq1o  36932  sumeq2si  36991  prodeq2si  36993  cbvprodvw2  37036  bj-snsetex  37876  bj-reabeq  37940  bj-rest10  38009  bj-ismooredr2  38031  bj-pinftynminfty  38148  dffinxpf  38308  finxp0  38314  ismblfin  38579  opropabco  38658  fdc  38679  isdrngo1  38890  smprngopr  38986  qseq  39665  eldisjlem19  39845  cdleme25cv  41415  cdlemk35  41969  dicval2  42236  dicopelval2  42238  dicelval2N  42239  hdmap1fval  42853  sn-0tie0  43515  absnw  43689  mzpcompact2lem  43761  eldioph4b  43817  2nn0ind  43951  islmodfg  44070  abeqabi  44408  relintab  44583  brtrclfv2  44726  frege116  44978  elnev  45420  dvnprodlem1  46955  fourierdlem103  47218  fourierdlem104  47219  ovnovollem3  47667  fmtno4prmfac  48656  usgrexmpl2nb1  49129  usgrexmpl2nb2  49130  usgrexmpl2nb3  49131  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  pgnioedg1  49205  pgnioedg2  49206  pgnioedg3  49207  pgnioedg4  49208  pgnioedg5  49209  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  pgnbgreunbgrlem5lem1  49217  pgnbgreunbgrlem5lem2  49218  pgnbgreunbgrlem5lem3  49219  smprngprmrng  49435  lindsrng01  49579  ldepspr  49584  nn0sumshdiglemB  49731  mofeu  49957  f1omo  50000  veronesevrowd  50978