Theorem eqeq2i 2752

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

Syntax hints:   ↔ wb 207   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqeq12i  2757  eqtri  2762  neeq2i  2999  rabid2f  3422  rabid2im  3423  abv  3443  equncom  4089  eq0  4278  ab0w  4307  ab0  4308  ab0orv  4311  absn  4575  rabrsn  4656  ssunpr  4765  sspr  4766  sstp  4767  preq12b  4781  preqsnd  4790  preq12nebg  4794  opthprneg  4796  opeqpr  5446  propssopi  5449  wefrc  5612  dfrel4v  6141  dfrel4  6142  orddif  6408  funopg  6519  f1imadifssran  6571  funcocnv2  6792  dffn5f  6898  fnressn  7101  fressnfv  7103  fnprb  7152  fntpb  7153  riotaeqimp  7339  fnov  7487  ovmpos  7504  onuninsuci  7780  fvresex  7902  elxp6  7965  el2xptp  7977  el2xptp0  7978  opiota  8001  tpossym  8198  qsid  8718  mapsncnv  8831  ixpsnf1o  8876  card1  9883  pm54.43lem  9915  cf0  10164  sdom2en01  10215  cardeq0  10465  enqbreq2  10834  addcompr  10935  mulcompr  10937  axrrecex  11077  negeq0  11439  muleqadd  11785  crne0  12143  dfnn3  12179  xmulneg1  13212  hasheq0  14316  hashbc  14406  hashf1lem2  14409  hash2pwpr  14429  eqwrds3  14914  cjne0  15116  sqrt00  15216  sqrtmsq2i  15341  cbvsum  15648  cbvsumv  15649  fsump1i  15722  cbvprod  15869  cbvprodv  15870  bpoly2  16013  bpoly3  16014  bpoly4  16015  absefib  16156  efieq1re  16157  xpccatid  18145  sgrpidmnd  18698  smndex2dnrinv  18877  isnsg4  19133  opprdomnb  20689  selvval  22096  mat1dimelbas  22454  pmatcollpw3fi1lem1  22769  2ndcctbss  23438  ptcnp  23605  ovolgelb  25465  ioorinv  25561  dvcobr  25931  rolle  25975  dvfsumlem2  26012  plymul0or  26265  reeff1o  26430  sineq0  26506  coseq1  26507  1cubr  26824  atandm2  26859  atandm3  26860  efrlim  26951  isppw  27095  ppiub  27185  lgsdinn0  27326  m1lgs  27369  elzs2  28409  elznns  28412  twocut  28433  uhgr2edg  29295  usgredg2vlem1  29312  usgredg2vlem2  29313  ushgredgedg  29316  ushgredgedgloop  29318  edgnbusgreu  29454  nb3grprlem2  29468  nb3gr2nb  29471  usgredgsscusgredg  29546  usgr2wlkneq  29842  usgr2pthlem  29849  crctcshwlkn0  29907  wwlksn0s  29947  umgr2adedgwlk  30031  umgr2adedgspth  30034  elwwlks2s3  30037  elwwlks2ons3im  30040  rusgrnumwwlkl1  30057  clwlkclwwlkflem  30092  isfrgr  30348  frgr3v  30363  frgrregorufr0  30412  isgrpo  30586  vciOLD  30650  chnlei  31574  h1de2ctlem  31644  cmcmlem  31680  cmcm2i  31682  cmbr2i  31685  osumcor2i  31733  pjss2i  31769  ho01i  31917  nmop0h  32080  pjclem1  32284  jplem1  32357  atabs2i  32491  1arithidom  33620  ply1dg1rt  33663  selvply1rhmlem2  33705  esplyfval1  33757  vieta  33764  fedgmullem2  33814  ccfldextdgrr  33856  zarcls  34058  breprexp  34817  bnj168  34913  bnj927  34952  bnj543  35075  bnj970  35129  subfacp1lem6  35413  satfv1  35591  satfvsucsuc  35593  satf0  35600  fmlaomn0  35618  fmla0disjsuc  35626  satffunlem2lem1  35632  mppspstlem  35799  quad3  35898  brdomain  36159  brrange  36160  brimg  36163  brapply  36164  lemsuccf  36167  brfullfun  36176  brrestrict  36177  rankeq1o  36399  sumeq2si  36430  prodeq2si  36432  cbvprodvw2  36475  bj-snsetex  37316  bj-reabeq  37380  bj-rest10  37446  bj-ismooredr2  37468  bj-pinftynminfty  37587  dffinxpf  37747  finxp0  37753  matunitlindflem1  37983  ismblfin  38028  opropabco  38091  fdc  38112  isdrngo1  38323  smprngopr  38419  qseq  39100  eldisjlem19  39280  cdleme25cv  40850  cdlemk35  41404  dicval2  41671  dicopelval2  41673  dicelval2N  41674  hdmap1fval  42288  sn-0tie0  42941  absnw  43128  mzpcompact2lem  43200  eldioph4b  43256  2nn0ind  43390  islmodfg  43514  abeqabi  43852  relintab  44027  brtrclfv2  44171  frege116  44423  elnev  44881  dvnprodlem1  46389  fourierdlem103  46652  fourierdlem104  46653  ovnovollem3  47101  fmtno4prmfac  48050  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  lindsrng01  48959  ldepspr  48964  nn0sumshdiglemB  49111  mofeu  49338  f1omo  49383