Theorem eqeq2i 2778

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 2777	. 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 2156  ax-ext 2737

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

This theorem is used by:  eqeq12i  2783  eqtri  2788  neeq2i  3025  rabid2f  3449  rabid2im  3450  abv  3469  equncom  4113  eq0  4304  ab0w  4335  ab0  4336  ab0orv  4339  absn  4611  rabrsn  4692  ssunpr  4801  sspr  4802  sstp  4803  preq12b  4817  preqsnd  4826  preq12nebg  4830  opthprneg  4832  opeqpr  5490  propssopi  5493  wefrc  5657  dfrel4v  6190  dfrel4  6191  orddif  6463  funopg  6574  funcocnv2  6850  dffn5f  6956  fnressn  7161  fressnfv  7163  fnprb  7213  fntpb  7214  riotaeqimp  7402  fnov  7550  ovmpos  7567  onuninsuci  7842  fvresex  7963  elxp6  8026  el2xptp  8038  el2xptp0  8039  opiota  8062  tpossym  8260  qsid  8785  mapsncnv  8897  ixpsnf1o  8942  card1  9970  pm54.43lem  10002  cf0  10249  sdom2en01  10301  cardeq0  10553  enqbreq2  10922  addcompr  11023  mulcompr  11025  axrrecex  11165  negeq0  11529  muleqadd  11875  crne0  12228  dfnn3  12264  xmulneg1  13313  hasheq0  14419  hashbc  14510  hashf1lem2  14513  hash2pwpr  14533  eqwrds3  15024  cjne0  15240  sqrt00  15340  sqrtmsq2i  15465  cbvsum  15772  cbvsumv  15773  fsump1i  15845  cbvprod  15992  cbvprodv  15993  bpoly2  16135  bpoly3  16136  bpoly4  16137  absefib  16278  efieq1re  16279  xpccatid  18268  sgrpidmnd  18831  smndex2dnrinv  19016  isnsg4  19279  opprdomnb  20867  selvval  22323  mat1dimelbas  22680  pmatcollpw3fi1lem1  22995  2ndcctbss  23665  ptcnp  23832  ovolgelb  25692  ioorinv  25788  dvcobr  26158  rolle  26202  dvfsumlem2  26239  plymul0or  26492  reeff1o  26663  sineq0  26742  coseq1  26743  1cubr  27060  atandm2  27095  atandm3  27096  efrlim  27187  isppw  27331  ppiub  27421  lgsdinn0  27562  m1lgs  27605  elzs2  28645  elznns  28648  twocut  28669  uhgr2edg  29618  usgredg2vlem1  29635  usgredg2vlem2  29636  ushgredgedg  29639  ushgredgedgloop  29641  edgnbusgreu  29777  nb3grprlem2  29791  nb3gr2nb  29794  usgredgsscusgredg  29869  usgr2wlkneq  30171  usgr2pthlem  30178  crctcshwlkn0  30239  wwlksn0s  30279  umgr2adedgwlk  30363  umgr2adedgspth  30366  elwwlks2s3  30369  elwwlks2ons3im  30372  rusgrnumwwlkl1  30389  clwlkclwwlkflem  30424  isfrgr  30684  frgr3v  30699  frgrregorufr0  30748  isgrpo  30922  vciOLD  30986  chnlei  31910  h1de2ctlem  31980  cmcmlem  32016  cmcm2i  32018  cmbr2i  32021  osumcor2i  32069  pjss2i  32105  ho01i  32253  nmop0h  32416  pjclem1  32620  jplem1  32693  atabs2i  32827  1arithidom  33893  ply1dg1rt  33936  selvply1rhmlem2  33977  esplyfval1  34029  vieta  34036  fedgmullem2  34086  ccfldextdgrr  34128  zarcls  34330  breprexp  35087  bnj168  35186  bnj927  35225  bnj543  35348  bnj970  35402  subfacp1lem6  35716  satfv1  35894  satfvsucsuc  35896  satf0  35903  fmlaomn0  35921  fmla0disjsuc  35929  satffunlem2lem1  35935  mppspstlem  36102  quad3  36201  brdomain  36462  brrange  36463  brimg  36466  brapply  36467  lemsuccf  36470  brfullfun  36479  brrestrict  36480  rankeq1o  36702  sumeq2si  36773  prodeq2si  36775  cbvprodvw2  36818  bj-snsetex  37658  bj-reabeq  37722  bj-rest10  37789  bj-ismooredr2  37811  bj-pinftynminfty  37930  dffinxpf  38090  finxp0  38096  matunitlindflem1  38326  ismblfin  38371  opropabco  38435  fdc  38456  isdrngo1  38667  smprngopr  38763  qseq  39442  eldisjlem19  39622  cdleme25cv  41192  cdlemk35  41746  dicval2  42013  dicopelval2  42015  dicelval2N  42016  hdmap1fval  42630  sn-0tie0  43285  absnw  43470  mzpcompact2lem  43542  eldioph4b  43598  2nn0ind  43732  islmodfg  43856  abeqabi  44194  relintab  44369  brtrclfv2  44513  frege116  44765  elnev  45207  dvnprodlem1  46720  fourierdlem103  46983  fourierdlem104  46984  ovnovollem3  47432  fmtno4prmfac  48384  usgrexmpl2nb1  48857  usgrexmpl2nb2  48858  usgrexmpl2nb3  48859  usgrexmpl2nb4  48860  usgrexmpl2nb5  48861  pgnioedg1  48933  pgnioedg2  48934  pgnioedg3  48935  pgnioedg4  48936  pgnioedg5  48937  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  pgnbgreunbgrlem2lem3  48941  pgnbgreunbgrlem5lem1  48945  pgnbgreunbgrlem5lem2  48946  pgnbgreunbgrlem5lem3  48947  smprngprmrng  49163  lindsrng01  49307  ldepspr  49312  nn0sumshdiglemB  49459  mofeu  49685  f1omo  49730