Theorem eqeq2i 2742

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeq12i  2747  eqtri  2752  neeq2i  2990  rabid2f  3434  rabid2im  3435  abv  3456  equncom  4118  eq0  4309  ab0w  4338  ab0  4339  ab0orv  4342  eq0rdv  4366  rzal  4468  absn  4605  rabrsn  4684  ssunpr  4794  sspr  4795  sstp  4796  preq12b  4810  preqsnd  4819  preq12nebg  4823  opthprneg  4825  opeqpr  5460  propssopi  5463  wefrc  5625  dfrel4v  6151  dfrel4  6152  orddif  6418  funopg  6534  f1imadifssran  6586  funcocnv2  6807  dffn5f  6914  fnressn  7112  fressnfv  7114  fnprb  7164  fntpb  7165  riotaeqimp  7352  fnov  7500  ovmpos  7517  onuninsuci  7796  fvresex  7918  elxp6  7981  el2xptp  7993  el2xptp0  7994  opiota  8017  tpossym  8214  qsid  8731  mapsncnv  8843  ixpsnf1o  8888  card1  9897  pm54.43lem  9929  cf0  10180  sdom2en01  10231  cardeq0  10481  enqbreq2  10849  addcompr  10950  mulcompr  10952  axrrecex  11092  negeq0  11452  muleqadd  11798  crne0  12155  dfnn3  12176  xmulneg1  13205  hasheq0  14304  hashbc  14394  hashf1lem2  14397  hash2pwpr  14417  eqwrds3  14903  cjne0  15105  sqrt00  15205  sqrtmsq2i  15330  cbvsum  15637  cbvsumv  15638  fsump1i  15711  cbvprod  15855  cbvprodv  15856  bpoly2  15999  bpoly3  16000  bpoly4  16001  absefib  16142  efieq1re  16143  xpccatid  18125  sgrpidmnd  18642  smndex2dnrinv  18818  isnsg4  19075  opprdomnb  20602  selvval  21998  mat1dimelbas  22334  pmatcollpw3fi1lem1  22649  2ndcctbss  23318  ptcnp  23485  ovolgelb  25357  ioorinv  25453  dvcobr  25825  rolle  25870  dvfsumlem2  25909  plymul0or  26164  reeff1o  26333  sineq0  26409  coseq1  26410  1cubr  26728  atandm2  26763  atandm3  26764  efrlim  26855  efrlimOLD  26856  isppw  27000  ppiub  27091  lgsdinn0  27232  m1lgs  27275  elzs2  28263  elznns  28266  1p1e2s  28278  twocut  28285  uhgr2edg  29111  usgredg2vlem1  29128  usgredg2vlem2  29129  ushgredgedg  29132  ushgredgedgloop  29134  edgnbusgreu  29270  nb3grprlem2  29284  nb3gr2nb  29287  usgredgsscusgredg  29363  usgr2wlkneq  29659  usgr2pthlem  29666  crctcshwlkn0  29724  wwlksn0s  29764  umgr2adedgwlk  29848  umgr2adedgspth  29851  elwwlks2s3  29854  elwwlks2ons3im  29857  rusgrnumwwlkl1  29871  clwlkclwwlkflem  29906  isfrgr  30162  frgr3v  30177  frgrregorufr0  30226  isgrpo  30399  vciOLD  30463  chnlei  31387  h1de2ctlem  31457  cmcmlem  31493  cmcm2i  31495  cmbr2i  31498  osumcor2i  31546  pjss2i  31582  ho01i  31730  nmop0h  31893  pjclem1  32097  jplem1  32170  atabs2i  32304  1arithidom  33481  ply1dg1rt  33521  fedgmullem2  33599  ccfldextdgrr  33640  zarcls  33837  breprexp  34597  bnj168  34693  bnj927  34732  bnj543  34856  bnj970  34910  subfacp1lem6  35145  satfv1  35323  satfvsucsuc  35325  satf0  35332  fmlaomn0  35350  fmla0disjsuc  35358  satffunlem2lem1  35364  mppspstlem  35531  quad3  35630  brdomain  35894  brrange  35895  brimg  35898  brapply  35899  brsuccf  35902  brfullfun  35909  brrestrict  35910  rankeq1o  36132  sumeq2si  36163  prodeq2si  36165  cbvprodvw2  36208  bj-snsetex  36924  bj-reabeq  36988  bj-rest10  37049  bj-ismooredr2  37071  bj-pinftynminfty  37188  dffinxpf  37346  finxp0  37352  matunitlindflem1  37583  ismblfin  37628  opropabco  37691  fdc  37712  isdrngo1  37923  smprngopr  38019  qseq  38613  eldisjlem19  38775  cdleme25cv  40325  cdlemk35  40879  dicval2  41146  dicopelval2  41148  dicelval2N  41149  hdmap1fval  41763  sn-0tie0  42412  absnw  42639  mzpcompact2lem  42712  eldioph4b  42772  2nn0ind  42907  islmodfg  43031  abeqabi  43370  relintab  43545  brtrclfv2  43689  frege116  43941  elnev  44400  dvnprodlem1  45917  fourierdlem103  46180  fourierdlem104  46181  ovnovollem3  46629  fmtno4prmfac  47546  usgrexmpl2nb1  47996  usgrexmpl2nb2  47997  usgrexmpl2nb3  47998  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  pgnioedg1  48071  pgnioedg2  48072  pgnioedg3  48073  pgnioedg4  48074  pgnioedg5  48075  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem5lem1  48083  pgnbgreunbgrlem5lem2  48084  pgnbgreunbgrlem5lem3  48085  lindsrng01  48430  ldepspr  48435  nn0sumshdiglemB  48582  mofeu  48809  f1omo  48854