Theorem eqeq2i 2478

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eqeq2i.1	|- A = B

Assertion

Ref	Expression
eqeq2i	|- ( C = A <-> C = B )

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 |- A = B
2		eqeq2 2475	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	ax-mp 5	1 |- ( C = A <-> C = B )

Syntax hints:   <-> wb 184   = wceq 1374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-cleq 2452

This theorem is referenced by:  eqeq12i  2480  eqtri  2489  neeq2i  2747  rabid2  3032  dfss2  3486  equncom  3642  rabrsn  4090  ssunpr  4182  sspr  4183  sstp  4184  preq12b  4195  preqsn  4202  opeqpr  4737  wefrc  4866  orddif  4964  dfrel4v  5449  dfiota2  5543  funopg  5611  funimaexg  5656  dffn5f  5913  fnressn  6064  fressnfv  6066  fnprb  6110  fnov  6385  ovmpt2s  6401  onuninsuci  6646  fvresex  6747  elxp6  6806  el2xptp  6817  el2xptp0  6818  opiota  6833  tpossym  6977  qsid  7367  mapsncnv  7455  ixpsnf1o  7499  card1  8338  pm54.43lem  8369  cf0  8620  sdom2en01  8671  cardeq0  8916  enqbreq2  9287  addcompr  9388  mulcompr  9390  axrrecex  9529  negeq0  9862  muleqadd  10182  crne0  10518  dfnn3  10539  xmulneg1  11450  hasheq0  12388  euhash1  12432  hashbc  12455  hashf1lem2  12458  hash2pwpr  12472  cjne0  12946  sqr00  13047  sqrmsq2i  13169  cbvsum  13466  fsump1i  13533  absefib  13783  efieq1re  13784  xpccatid  15304  isnsg4  16032  mat1dimelbas  18733  pmatcollpw3fi1lem1  19047  2ndcctbss  19715  ptcnp  19851  ovolgelb  21619  ioorinv  21713  rolle  22119  plymul0or  22404  reeff1o  22569  sineq0  22640  coseq1  22641  1cubr  22894  atandm2  22929  atandm3  22930  efrlim  23020  isppw  23109  ppiub  23200  lgsdinn0  23336  m1lgs  23358  usgra2edg  24044  usgraedg4  24049  usgraidx2vlem1  24053  usgraidx2vlem2  24054  nb3graprlem2  24114  nb3grapr  24115  nb3grapr2  24116  nb3gra2nb  24117  2trllemH  24216  2trllemE  24217  usgrcyclnl2  24303  4cycl4dv  24329  wwlkn0  24351  wwlkn0s  24367  rusgranumwlkl1  24609  2pthfrgra  24673  isgrpo  24860  vci  25103  chnlei  26065  h1de2ctlem  26135  cmcmlem  26171  cmcm2i  26173  cmbr2i  26176  osumcor2i  26224  pjss2i  26260  ho01i  26409  nmop0h  26572  pjclem1  26776  jplem1  26849  atabs2i  26983  rabid2f  27062  preqsnd  27078  dfrel4  27113  subfacp1lem6  28255  quad3  28485  cbvprod  28610  trpredmintr  28877  brdomain  29146  brrange  29147  brimg  29150  brapply  29151  brsuccf  29154  brfullfun  29161  brrestrict  29162  bpoly2  29382  bpoly3  29383  bpoly4  29384  rankeq1o  29391  ismblfin  29619  opropabco  29804  fdc  29828  isdrngo1  29949  smprngopr  30039  mzpcompact2lem  30275  eldioph4b  30336  2nn0ind  30472  islmodfg  30608  elnev  30878  iccdifioo  31074  fourierdlem103  31465  fourierdlem104  31466  fourierswlem  31486  usgra2pthlem1  31777  usgedgvadf1lem1  31815  usgedgvadf1lem2  31816  usgedgvadf1ALTlem1  31818  usgedgvadf1ALTlem2  31819  lindsrng01  32017  ldepspr  32022  comraddi  32133  bnj168  32740  bnj927  32781  bnj543  32905  bnj970  32959  bj-snsetex  33477  bj-pinftynminfty  33577  cdleme25cv  35029  cdlemk35  35583  dicval2  35851  dicopelval2  35853  dicelval2N  35854  hdmap1fval  36469