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 209   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  eqeq12i  2751  eqtri  2759  neeq2i  2997  rabid2  3283  rabid2f  3284  abv  3409  dfss2OLD  3874  equncom  4054  eq0  4244  ab0w  4274  ab0  4275  ab0OLD  4276  ab0orv  4279  eq0rdv  4305  rzal  4406  absn  4545  rabrsn  4626  ssunpr  4731  sspr  4732  sstp  4733  preq12b  4747  preqsnd  4755  preq12nebg  4759  opthprneg  4761  opeqpr  5373  propssopi  5376  wefrc  5530  dfrel4v  6033  dfrel4  6034  orddif  6284  funopg  6392  funimaexg  6444  funcocnv2  6663  dffn5f  6761  fnressn  6951  fressnfv  6953  fnprb  7002  fntpb  7003  riotaeqimp  7175  fnov  7319  ovmpos  7335  onuninsuci  7597  fvresex  7711  elxp6  7773  el2xptp  7785  el2xptp0  7786  opiota  7807  tpossym  7978  qsid  8443  mapsncnv  8552  ixpsnf1o  8597  trpredmintr  9314  card1  9549  pm54.43lem  9581  cf0  9830  sdom2en01  9881  cardeq0  10131  enqbreq2  10499  addcompr  10600  mulcompr  10602  axrrecex  10742  negeq0  11097  muleqadd  11441  crne0  11788  dfnn3  11809  xmulneg1  12824  hasheq0  13895  hashbc  13982  hashf1lem2  13987  hash2pwpr  14007  eqwrds3  14493  cjne0  14691  sqrt00  14792  sqrtmsq2i  14916  cbvsum  15224  fsump1i  15296  cbvprod  15440  bpoly2  15582  bpoly3  15583  bpoly4  15584  absefib  15722  efieq1re  15723  xpccatid  17649  sgrpidmnd  18132  smndex2dnrinv  18296  isnsg4  18537  selvval  21032  mat1dimelbas  21322  pmatcollpw3fi1lem1  21637  2ndcctbss  22306  ptcnp  22473  ovolgelb  24331  ioorinv  24427  rolle  24841  plymul0or  25128  reeff1o  25293  sineq0  25367  coseq1  25368  1cubr  25679  atandm2  25714  atandm3  25715  efrlim  25806  isppw  25950  ppiub  26039  lgsdinn0  26180  m1lgs  26223  uhgr2edg  27250  usgredg2vlem1  27267  usgredg2vlem2  27268  ushgredgedg  27271  ushgredgedgloop  27273  edgnbusgreu  27409  nb3grprlem2  27423  nb3gr2nb  27426  usgredgsscusgredg  27501  usgr2wlkneq  27797  usgr2pthlem  27804  crctcshwlkn0  27859  wwlksn0s  27899  umgr2adedgwlk  27983  umgr2adedgspth  27986  elwwlks2s3  27989  elwwlks2ons3im  27992  rusgrnumwwlkl1  28006  clwlkclwwlkflem  28041  isfrgr  28297  frgr3v  28312  frgrregorufr0  28361  isgrpo  28532  vciOLD  28596  chnlei  29520  h1de2ctlem  29590  cmcmlem  29626  cmcm2i  29628  cmbr2i  29631  osumcor2i  29679  pjss2i  29715  ho01i  29863  nmop0h  30026  pjclem1  30230  jplem1  30303  atabs2i  30437  fedgmullem2  31379  ccfldextdgrr  31410  zarcls  31492  breprexp  32279  bnj168  32375  bnj927  32415  bnj543  32540  bnj970  32594  subfacp1lem6  32814  satfv1  32992  satfvsucsuc  32994  satf0  33001  fmlaomn0  33019  fmla0disjsuc  33027  satffunlem2lem1  33033  mppspstlem  33200  quad3  33295  brdomain  33921  brrange  33922  brimg  33925  brapply  33926  brsuccf  33929  brfullfun  33936  brrestrict  33937  rankeq1o  34159  bj-snsetex  34839  bj-reabeq  34903  bj-rest10  34943  bj-ismooredr2  34965  bj-pinftynminfty  35082  dffinxpf  35242  finxp0  35248  matunitlindflem1  35459  ismblfin  35504  opropabco  35568  fdc  35589  isdrngo1  35800  smprngopr  35896  cdleme25cv  38058  cdlemk35  38612  dicval2  38879  dicopelval2  38881  dicelval2N  38882  hdmap1fval  39496  sn-0tie0  40070  mzpcompact2lem  40217  eldioph4b  40277  2nn0ind  40411  islmodfg  40538  relintab  40808  brtrclfv2  40953  frege116  41205  elnev  41670  dvnprodlem1  43105  fourierdlem103  43368  fourierdlem104  43369  ovnovollem3  43814  fmtno4prmfac  44640  lindsrng01  45425  ldepspr  45430  nn0sumshdiglemB  45582  mofeu  45791