Theorem eqeq2i 2749

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

Syntax hints:   ↔ wb 206   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  eqeq12i  2754  eqtri  2759  neeq2i  2997  rabid2f  3420  rabid2im  3421  abv  3441  equncom  4099  eq0  4290  ab0w  4319  ab0  4320  ab0orv  4323  absn  4587  rabrsn  4668  ssunpr  4777  sspr  4778  sstp  4779  preq12b  4793  preqsnd  4802  preq12nebg  4806  opthprneg  4808  opeqpr  5459  propssopi  5462  wefrc  5625  dfrel4v  6154  dfrel4  6155  orddif  6421  funopg  6532  f1imadifssran  6584  funcocnv2  6805  dffn5f  6911  fnressn  7112  fressnfv  7114  fnprb  7163  fntpb  7164  riotaeqimp  7350  fnov  7498  ovmpos  7515  onuninsuci  7791  fvresex  7913  elxp6  7976  el2xptp  7988  el2xptp0  7989  opiota  8012  tpossym  8208  qsid  8728  mapsncnv  8841  ixpsnf1o  8886  card1  9892  pm54.43lem  9924  cf0  10173  sdom2en01  10224  cardeq0  10474  enqbreq2  10843  addcompr  10944  mulcompr  10946  axrrecex  11086  negeq0  11448  muleqadd  11794  crne0  12152  dfnn3  12188  xmulneg1  13221  hasheq0  14325  hashbc  14415  hashf1lem2  14418  hash2pwpr  14438  eqwrds3  14923  cjne0  15125  sqrt00  15225  sqrtmsq2i  15350  cbvsum  15657  cbvsumv  15658  fsump1i  15731  cbvprod  15878  cbvprodv  15879  bpoly2  16022  bpoly3  16023  bpoly4  16024  absefib  16165  efieq1re  16166  xpccatid  18154  sgrpidmnd  18707  smndex2dnrinv  18886  isnsg4  19142  opprdomnb  20694  selvval  22101  mat1dimelbas  22436  pmatcollpw3fi1lem1  22751  2ndcctbss  23420  ptcnp  23587  ovolgelb  25447  ioorinv  25543  dvcobr  25913  rolle  25957  dvfsumlem2  25994  plymul0or  26247  reeff1o  26412  sineq0  26488  coseq1  26489  1cubr  26806  atandm2  26841  atandm3  26842  efrlim  26933  isppw  27077  ppiub  27167  lgsdinn0  27308  m1lgs  27351  elzs2  28391  elznns  28394  twocut  28415  uhgr2edg  29277  usgredg2vlem1  29294  usgredg2vlem2  29295  ushgredgedg  29298  ushgredgedgloop  29300  edgnbusgreu  29436  nb3grprlem2  29450  nb3gr2nb  29453  usgredgsscusgredg  29528  usgr2wlkneq  29824  usgr2pthlem  29831  crctcshwlkn0  29889  wwlksn0s  29929  umgr2adedgwlk  30013  umgr2adedgspth  30016  elwwlks2s3  30019  elwwlks2ons3im  30022  rusgrnumwwlkl1  30039  clwlkclwwlkflem  30074  isfrgr  30330  frgr3v  30345  frgrregorufr0  30394  isgrpo  30568  vciOLD  30632  chnlei  31556  h1de2ctlem  31626  cmcmlem  31662  cmcm2i  31664  cmbr2i  31667  osumcor2i  31715  pjss2i  31751  ho01i  31899  nmop0h  32062  pjclem1  32266  jplem1  32339  atabs2i  32473  1arithidom  33597  ply1dg1rt  33640  esplyfval1  33717  vieta  33724  fedgmullem2  33774  ccfldextdgrr  33816  zarcls  34018  breprexp  34777  bnj168  34873  bnj927  34912  bnj543  35035  bnj970  35089  subfacp1lem6  35367  satfv1  35545  satfvsucsuc  35547  satf0  35554  fmlaomn0  35572  fmla0disjsuc  35580  satffunlem2lem1  35586  mppspstlem  35753  quad3  35852  brdomain  36113  brrange  36114  brimg  36117  brapply  36118  lemsuccf  36121  brfullfun  36130  brrestrict  36131  rankeq1o  36353  sumeq2si  36384  prodeq2si  36386  cbvprodvw2  36429  bj-snsetex  37270  bj-reabeq  37334  bj-rest10  37400  bj-ismooredr2  37422  bj-pinftynminfty  37541  dffinxpf  37701  finxp0  37707  matunitlindflem1  37937  ismblfin  37982  opropabco  38045  fdc  38066  isdrngo1  38277  smprngopr  38373  qseq  39054  eldisjlem19  39234  cdleme25cv  40804  cdlemk35  41358  dicval2  41625  dicopelval2  41627  dicelval2N  41628  hdmap1fval  42242  sn-0tie0  42896  absnw  43111  mzpcompact2lem  43183  eldioph4b  43239  2nn0ind  43373  islmodfg  43497  abeqabi  43835  relintab  44010  brtrclfv2  44154  frege116  44406  elnev  44864  dvnprodlem1  46374  fourierdlem103  46637  fourierdlem104  46638  ovnovollem3  47086  fmtno4prmfac  48035  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  lindsrng01  48944  ldepspr  48949  nn0sumshdiglemB  49096  mofeu  49323  f1omo  49368