Theorem eqeq2i 2782

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

Syntax hints:   ↔ wb 209   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqeq12i  2787  eqtri  2792  neeq2i  3029  rabid2f  3454  rabid2im  3455  abv  3475  equncom  4121  eq0  4312  ab0w  4342  ab0  4343  ab0orv  4346  absn  4614  rabrsn  4695  ssunpr  4803  sspr  4804  sstp  4805  preq12b  4819  preqsnd  4828  preq12nebg  4832  opthprneg  4834  opeqpr  5489  propssopi  5492  wefrc  5656  dfrel4v  6189  dfrel4  6190  orddif  6460  funopg  6571  funcocnv2  6847  dffn5f  6953  fnressn  7156  fressnfv  7158  fnprb  7207  fntpb  7208  riotaeqimp  7394  fnov  7542  ovmpos  7559  onuninsuci  7835  fvresex  7956  elxp6  8019  el2xptp  8031  el2xptp0  8032  opiota  8055  tpossym  8253  qsid  8778  mapsncnv  8890  ixpsnf1o  8935  card1  9953  pm54.43lem  9985  cf0  10233  sdom2en01  10285  cardeq0  10535  enqbreq2  10904  addcompr  11005  mulcompr  11007  axrrecex  11147  negeq0  11511  muleqadd  11857  crne0  12210  dfnn3  12246  xmulneg1  13294  hasheq0  14398  hashbc  14489  hashf1lem2  14492  hash2pwpr  14512  eqwrds3  14997  cjne0  15213  sqrt00  15313  sqrtmsq2i  15438  cbvsum  15745  cbvsumv  15746  fsump1i  15819  cbvprod  15966  cbvprodv  15967  bpoly2  16110  bpoly3  16111  bpoly4  16112  absefib  16253  efieq1re  16254  xpccatid  18243  sgrpidmnd  18796  smndex2dnrinv  18976  isnsg4  19232  opprdomnb  20800  selvval  22239  mat1dimelbas  22596  pmatcollpw3fi1lem1  22911  2ndcctbss  23580  ptcnp  23747  ovolgelb  25607  ioorinv  25703  dvcobr  26073  rolle  26117  dvfsumlem2  26154  plymul0or  26407  reeff1o  26575  sineq0  26654  coseq1  26655  1cubr  26972  atandm2  27007  atandm3  27008  efrlim  27099  isppw  27243  ppiub  27333  lgsdinn0  27474  m1lgs  27517  elzs2  28557  elznns  28560  twocut  28581  uhgr2edg  29498  usgredg2vlem1  29515  usgredg2vlem2  29516  ushgredgedg  29519  ushgredgedgloop  29521  edgnbusgreu  29657  nb3grprlem2  29671  nb3gr2nb  29674  usgredgsscusgredg  29749  usgr2wlkneq  30045  usgr2pthlem  30052  crctcshwlkn0  30110  wwlksn0s  30150  umgr2adedgwlk  30234  umgr2adedgspth  30237  elwwlks2s3  30240  elwwlks2ons3im  30243  rusgrnumwwlkl1  30260  clwlkclwwlkflem  30295  isfrgr  30551  frgr3v  30566  frgrregorufr0  30615  isgrpo  30789  vciOLD  30853  chnlei  31777  h1de2ctlem  31847  cmcmlem  31883  cmcm2i  31885  cmbr2i  31888  osumcor2i  31936  pjss2i  31972  ho01i  32120  nmop0h  32283  pjclem1  32487  jplem1  32560  atabs2i  32694  1arithidom  33771  ply1dg1rt  33814  selvply1rhmlem2  33855  esplyfval1  33907  vieta  33914  fedgmullem2  33964  ccfldextdgrr  34006  zarcls  34208  breprexp  34964  bnj168  35063  bnj927  35102  bnj543  35225  bnj970  35279  subfacp1lem6  35575  satfv1  35753  satfvsucsuc  35755  satf0  35762  fmlaomn0  35780  fmla0disjsuc  35788  satffunlem2lem1  35794  mppspstlem  35961  quad3  36060  brdomain  36321  brrange  36322  brimg  36325  brapply  36326  lemsuccf  36329  brfullfun  36338  brrestrict  36339  rankeq1o  36561  sumeq2si  36602  prodeq2si  36604  cbvprodvw2  36647  bj-snsetex  37486  bj-reabeq  37550  bj-rest10  37617  bj-ismooredr2  37639  bj-pinftynminfty  37758  dffinxpf  37918  finxp0  37924  matunitlindflem1  38154  ismblfin  38199  opropabco  38262  fdc  38283  isdrngo1  38494  smprngopr  38590  qseq  39271  eldisjlem19  39451  cdleme25cv  41021  cdlemk35  41575  dicval2  41842  dicopelval2  41844  dicelval2N  41845  hdmap1fval  42459  sn-0tie0  43114  absnw  43301  mzpcompact2lem  43373  eldioph4b  43429  2nn0ind  43563  islmodfg  43687  abeqabi  44025  relintab  44200  brtrclfv2  44344  frege116  44596  elnev  45038  dvnprodlem1  46551  fourierdlem103  46814  fourierdlem104  46815  ovnovollem3  47263  fmtno4prmfac  48212  usgrexmpl2nb1  48685  usgrexmpl2nb2  48686  usgrexmpl2nb3  48687  usgrexmpl2nb4  48688  usgrexmpl2nb5  48689  pgnioedg1  48761  pgnioedg2  48762  pgnioedg3  48763  pgnioedg4  48764  pgnioedg5  48765  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  pgnbgreunbgrlem2lem3  48769  pgnbgreunbgrlem5lem1  48773  pgnbgreunbgrlem5lem2  48774  pgnbgreunbgrlem5lem3  48775  smprngprmrng  48992  lindsrng01  49132  ldepspr  49137  nn0sumshdiglemB  49284  mofeu  49510  f1omo  49555