Theorem eqeq2i 2747

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

Syntax hints:   ↔ wb 206   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  eqeq12i  2752  eqtri  2762  neeq2i  3003  rabid2f  3465  rabid2im  3466  rabid2OLD  3468  abv  3489  equncom  4168  eq0  4355  ab0w  4384  ab0  4385  ab0orv  4388  eq0rdv  4412  rzal  4514  absn  4649  rabrsn  4728  ssunpr  4838  sspr  4839  sstp  4840  preq12b  4854  preqsnd  4863  preq12nebg  4867  opthprneg  4869  opeqpr  5514  propssopi  5517  wefrc  5682  dfrel4v  6211  dfrel4  6212  orddif  6481  funopg  6601  funimaexgOLD  6654  funcocnv2  6873  dffn5f  6979  fnressn  7177  fressnfv  7179  fnprb  7227  fntpb  7228  riotaeqimp  7413  fnov  7563  ovmpos  7580  onuninsuci  7860  fvresex  7982  elxp6  8046  el2xptp  8058  el2xptp0  8059  opiota  8082  tpossym  8281  dfwrecsOLD  8336  qsid  8821  mapsncnv  8931  ixpsnf1o  8976  card1  10005  pm54.43lem  10037  cf0  10288  sdom2en01  10339  cardeq0  10589  enqbreq2  10957  addcompr  11058  mulcompr  11060  axrrecex  11200  negeq0  11560  muleqadd  11904  crne0  12256  dfnn3  12277  xmulneg1  13307  hasheq0  14398  hashbc  14488  hashf1lem2  14491  hash2pwpr  14511  eqwrds3  14996  cjne0  15198  sqrt00  15298  sqrtmsq2i  15422  cbvsum  15727  cbvsumv  15728  fsump1i  15801  cbvprod  15945  cbvprodv  15946  bpoly2  16089  bpoly3  16090  bpoly4  16091  absefib  16230  efieq1re  16231  xpccatid  18243  sgrpidmnd  18764  smndex2dnrinv  18940  isnsg4  19197  opprdomnb  20733  selvval  22156  mat1dimelbas  22492  pmatcollpw3fi1lem1  22807  2ndcctbss  23478  ptcnp  23645  ovolgelb  25528  ioorinv  25624  dvcobr  25997  rolle  26042  dvfsumlem2  26081  plymul0or  26336  reeff1o  26505  sineq0  26580  coseq1  26581  1cubr  26899  atandm2  26934  atandm3  26935  efrlim  27026  efrlimOLD  27027  isppw  27171  ppiub  27262  lgsdinn0  27403  m1lgs  27446  elzs2  28399  elznns  28402  1p1e2s  28414  uhgr2edg  29239  usgredg2vlem1  29256  usgredg2vlem2  29257  ushgredgedg  29260  ushgredgedgloop  29262  edgnbusgreu  29398  nb3grprlem2  29412  nb3gr2nb  29415  usgredgsscusgredg  29491  usgr2wlkneq  29788  usgr2pthlem  29795  crctcshwlkn0  29850  wwlksn0s  29890  umgr2adedgwlk  29974  umgr2adedgspth  29977  elwwlks2s3  29980  elwwlks2ons3im  29983  rusgrnumwwlkl1  29997  clwlkclwwlkflem  30032  isfrgr  30288  frgr3v  30303  frgrregorufr0  30352  isgrpo  30525  vciOLD  30589  chnlei  31513  h1de2ctlem  31583  cmcmlem  31619  cmcm2i  31621  cmbr2i  31624  osumcor2i  31672  pjss2i  31708  ho01i  31856  nmop0h  32019  pjclem1  32223  jplem1  32296  atabs2i  32430  1arithidom  33544  ply1dg1rt  33583  fedgmullem2  33657  ccfldextdgrr  33696  zarcls  33834  breprexp  34626  bnj168  34722  bnj927  34761  bnj543  34885  bnj970  34939  subfacp1lem6  35169  satfv1  35347  satfvsucsuc  35349  satf0  35356  fmlaomn0  35374  fmla0disjsuc  35382  satffunlem2lem1  35388  mppspstlem  35555  quad3  35654  brdomain  35914  brrange  35915  brimg  35918  brapply  35919  brsuccf  35922  brfullfun  35929  brrestrict  35930  rankeq1o  36152  sumeq2si  36183  prodeq2si  36185  cbvprodvw2  36229  bj-snsetex  36945  bj-reabeq  37009  bj-rest10  37070  bj-ismooredr2  37092  bj-pinftynminfty  37209  dffinxpf  37367  finxp0  37373  matunitlindflem1  37602  ismblfin  37647  opropabco  37710  fdc  37731  isdrngo1  37942  smprngopr  38038  eldisjlem19  38791  cdleme25cv  40340  cdlemk35  40894  dicval2  41161  dicopelval2  41163  dicelval2N  41164  hdmap1fval  41778  sn-0tie0  42445  absnw  42664  mzpcompact2lem  42738  eldioph4b  42798  2nn0ind  42933  islmodfg  43057  abeqabi  43397  relintab  43572  brtrclfv2  43716  frege116  43968  elnev  44433  dvnprodlem1  45901  fourierdlem103  46164  fourierdlem104  46165  ovnovollem3  46613  fmtno4prmfac  47496  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  lindsrng01  48313  ldepspr  48318  nn0sumshdiglemB  48469  mofeu  48677