Theorem eqeq2i 2748

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 2747	. 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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eqeq12i  2753  eqtri  2758  neeq2i  2997  rabid2f  3447  rabid2im  3448  rabid2OLD  3450  abv  3471  equncom  4134  eq0  4325  ab0w  4354  ab0  4355  ab0orv  4358  eq0rdv  4382  rzal  4484  absn  4621  rabrsn  4700  ssunpr  4810  sspr  4811  sstp  4812  preq12b  4826  preqsnd  4835  preq12nebg  4839  opthprneg  4841  opeqpr  5480  propssopi  5483  wefrc  5648  dfrel4v  6179  dfrel4  6180  orddif  6449  funopg  6569  f1imadifssran  6621  funimaexgOLD  6623  funcocnv2  6842  dffn5f  6949  fnressn  7147  fressnfv  7149  fnprb  7199  fntpb  7200  riotaeqimp  7386  fnov  7536  ovmpos  7553  onuninsuci  7833  fvresex  7956  elxp6  8020  el2xptp  8032  el2xptp0  8033  opiota  8056  tpossym  8255  dfwrecsOLD  8310  qsid  8795  mapsncnv  8905  ixpsnf1o  8950  card1  9980  pm54.43lem  10012  cf0  10263  sdom2en01  10314  cardeq0  10564  enqbreq2  10932  addcompr  11033  mulcompr  11035  axrrecex  11175  negeq0  11535  muleqadd  11879  crne0  12231  dfnn3  12252  xmulneg1  13283  hasheq0  14379  hashbc  14469  hashf1lem2  14472  hash2pwpr  14492  eqwrds3  14978  cjne0  15180  sqrt00  15280  sqrtmsq2i  15404  cbvsum  15709  cbvsumv  15710  fsump1i  15783  cbvprod  15927  cbvprodv  15928  bpoly2  16071  bpoly3  16072  bpoly4  16073  absefib  16214  efieq1re  16215  xpccatid  18198  sgrpidmnd  18715  smndex2dnrinv  18891  isnsg4  19148  opprdomnb  20675  selvval  22071  mat1dimelbas  22407  pmatcollpw3fi1lem1  22722  2ndcctbss  23391  ptcnp  23558  ovolgelb  25431  ioorinv  25527  dvcobr  25899  rolle  25944  dvfsumlem2  25983  plymul0or  26238  reeff1o  26407  sineq0  26483  coseq1  26484  1cubr  26802  atandm2  26837  atandm3  26838  efrlim  26929  efrlimOLD  26930  isppw  27074  ppiub  27165  lgsdinn0  27306  m1lgs  27349  elzs2  28302  elznns  28305  1p1e2s  28317  uhgr2edg  29133  usgredg2vlem1  29150  usgredg2vlem2  29151  ushgredgedg  29154  ushgredgedgloop  29156  edgnbusgreu  29292  nb3grprlem2  29306  nb3gr2nb  29309  usgredgsscusgredg  29385  usgr2wlkneq  29684  usgr2pthlem  29691  crctcshwlkn0  29749  wwlksn0s  29789  umgr2adedgwlk  29873  umgr2adedgspth  29876  elwwlks2s3  29879  elwwlks2ons3im  29882  rusgrnumwwlkl1  29896  clwlkclwwlkflem  29931  isfrgr  30187  frgr3v  30202  frgrregorufr0  30251  isgrpo  30424  vciOLD  30488  chnlei  31412  h1de2ctlem  31482  cmcmlem  31518  cmcm2i  31520  cmbr2i  31523  osumcor2i  31571  pjss2i  31607  ho01i  31755  nmop0h  31918  pjclem1  32122  jplem1  32195  atabs2i  32329  1arithidom  33498  ply1dg1rt  33538  fedgmullem2  33616  ccfldextdgrr  33659  zarcls  33851  breprexp  34611  bnj168  34707  bnj927  34746  bnj543  34870  bnj970  34924  subfacp1lem6  35153  satfv1  35331  satfvsucsuc  35333  satf0  35340  fmlaomn0  35358  fmla0disjsuc  35366  satffunlem2lem1  35372  mppspstlem  35539  quad3  35638  brdomain  35897  brrange  35898  brimg  35901  brapply  35902  brsuccf  35905  brfullfun  35912  brrestrict  35913  rankeq1o  36135  sumeq2si  36166  prodeq2si  36168  cbvprodvw2  36211  bj-snsetex  36927  bj-reabeq  36991  bj-rest10  37052  bj-ismooredr2  37074  bj-pinftynminfty  37191  dffinxpf  37349  finxp0  37355  matunitlindflem1  37586  ismblfin  37631  opropabco  37694  fdc  37715  isdrngo1  37926  smprngopr  38022  eldisjlem19  38774  cdleme25cv  40323  cdlemk35  40877  dicval2  41144  dicopelval2  41146  dicelval2N  41147  hdmap1fval  41761  sn-0tie0  42429  absnw  42648  mzpcompact2lem  42721  eldioph4b  42781  2nn0ind  42916  islmodfg  43040  abeqabi  43379  relintab  43554  brtrclfv2  43698  frege116  43950  elnev  44410  dvnprodlem1  45923  fourierdlem103  46186  fourierdlem104  46187  ovnovollem3  46635  fmtno4prmfac  47534  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  lindsrng01  48392  ldepspr  48397  nn0sumshdiglemB  48548  mofeu  48774