Theorem eqeq2i 2773

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 2772	. 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 2155  ax-ext 2732

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

This theorem is used by:  eqeq12i  2778  eqtri  2783  neeq2i  3020  rabid2f  3442  rabid2im  3443  abv  3462  equncom  4106  eq0  4297  ab0w  4328  ab0  4329  ab0orv  4332  absn  4604  rabrsn  4685  ssunpr  4794  sspr  4795  sstp  4796  preq12b  4810  preqsnd  4819  preq12nebg  4823  opthprneg  4825  opeqpr  5482  propssopi  5485  wefrc  5649  dfrel4v  6183  dfrel4  6184  orddif  6456  funopg  6568  funcocnv2  6844  dffn5f  6950  fnressn  7156  fressnfv  7158  fnprb  7208  fntpb  7209  riotaeqimp  7397  fnov  7545  ovmpos  7562  onuninsuci  7837  fvresex  7958  elxp6  8021  el2xptp  8033  el2xptp0  8034  opiota  8057  tpossym  8257  qsid  8782  mapsncnv  8901  ixpsnf1o  8946  card1  9974  pm54.43lem  10006  cf0  10253  sdom2en01  10305  cardeq0  10561  enqbreq2  10930  addcompr  11031  mulcompr  11033  axrrecex  11173  negeq0  11537  muleqadd  11883  crne0  12236  dfnn3  12272  xmulneg1  13322  hasheq0  14428  hashbc  14519  hashf1lem2  14522  hash2pwpr  14542  eqwrds3  15035  cjne0  15251  sqrt00  15351  sqrtmsq2i  15476  cbvsum  15783  cbvsumv  15784  fsump1i  15856  cbvprod  16003  cbvprodv  16004  bpoly2  16144  bpoly3  16145  bpoly4  16146  absefib  16287  efieq1re  16288  xpccatid  18277  sgrpidmnd  18842  smndex2dnrinv  19028  isnsg4  19291  opprdomnb  20879  selvval  22337  mat1dimelbas  22694  matunitlindflem1  22902  pmatcollpw3fi1lem1  23012  2ndcctbss  23682  ptcnp  23849  ovolgelb  25709  ioorinv  25805  dvcobr  26174  rolle  26218  dvfsumlem2  26255  plymul0or  26509  reeff1o  26684  sineq0  26762  coseq1  26763  1cubr  27080  atandm2  27115  atandm3  27116  efrlim  27207  isppw  27351  ppiub  27441  lgsdinn0  27582  m1lgs  27625  elzs2  28665  elznns  28668  twocut  28689  uhgr2edg  29669  usgredg2vlem1  29686  usgredg2vlem2  29687  ushgredgedg  29690  ushgredgedgloop  29692  edgnbusgreu  29828  nb3grprlem2  29842  nb3gr2nb  29845  usgredgsscusgredg  29920  usgr2wlkneq  30222  usgr2pthlem  30229  crctcshwlkn0  30290  wwlksn0s  30330  umgr2adedgwlk  30414  umgr2adedgspth  30417  elwwlks2s3  30420  elwwlks2ons3im  30423  rusgrnumwwlkl1  30440  clwlkclwwlkflem  30475  isfrgr  30741  frgr3v  30756  frgrregorufr0  30805  isgrpo  30979  vciOLD  31043  chnlei  31967  h1de2ctlem  32037  cmcmlem  32073  cmcm2i  32075  cmbr2i  32078  osumcor2i  32126  pjss2i  32162  ho01i  32310  nmop0h  32473  pjclem1  32677  jplem1  32750  atabs2i  32884  1arithidom  33948  ply1dg1rt  33991  selvply1rhmlem2  34032  esplyfval1  34084  vieta  34091  fedgmullem2  34141  ccfldextdgrr  34183  zarcls  34385  breprexp  35142  bnj168  35241  bnj927  35280  bnj543  35403  bnj970  35457  subfacp1lem6  35765  satfv1  35943  satfvsucsuc  35945  satf0  35952  fmlaomn0  35970  fmla0disjsuc  35978  satffunlem2lem1  35984  mppspstlem  36151  quad3  36250  brdomain  36511  brrange  36512  brimg  36515  brapply  36516  lemsuccf  36519  brfullfun  36528  brrestrict  36529  rankeq1o  36752  sumeq2si  36823  prodeq2si  36825  cbvprodvw2  36868  bj-snsetex  37708  bj-reabeq  37772  bj-rest10  37839  bj-ismooredr2  37861  bj-pinftynminfty  37980  dffinxpf  38140  finxp0  38146  ismblfin  38411  opropabco  38475  fdc  38496  isdrngo1  38707  smprngopr  38803  qseq  39482  eldisjlem19  39662  cdleme25cv  41232  cdlemk35  41786  dicval2  42053  dicopelval2  42055  dicelval2N  42056  hdmap1fval  42670  sn-0tie0  43340  absnw  43525  mzpcompact2lem  43597  eldioph4b  43653  2nn0ind  43787  islmodfg  43911  abeqabi  44249  relintab  44424  brtrclfv2  44568  frege116  44820  elnev  45262  dvnprodlem1  46775  fourierdlem103  47038  fourierdlem104  47039  ovnovollem3  47487  fmtno4prmfac  48476  usgrexmpl2nb1  48949  usgrexmpl2nb2  48950  usgrexmpl2nb3  48951  usgrexmpl2nb4  48952  usgrexmpl2nb5  48953  pgnioedg1  49025  pgnioedg2  49026  pgnioedg3  49027  pgnioedg4  49028  pgnioedg5  49029  pgnbgreunbgrlem2lem1  49031  pgnbgreunbgrlem2lem2  49032  pgnbgreunbgrlem2lem3  49033  pgnbgreunbgrlem5lem1  49037  pgnbgreunbgrlem5lem2  49038  pgnbgreunbgrlem5lem3  49039  smprngprmrng  49255  lindsrng01  49399  ldepspr  49404  nn0sumshdiglemB  49551  mofeu  49777  f1omo  49820  veronesevrowd  50813