Theorem eqeq1i 2765

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq1i	⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq1 2764	. 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  eqabb  2899  neeq1i  3019  dfss2  3917  ssequn2  4135  ineqcom  4156  dfss7  4197  dfss4  4215  inssdif0  4322  rabeq0w  4337  rabeq0  4338  disj  4403  undisj1  4415  undisj2  4416  undif  4438  undifr  4439  rabeqsn  4628  reusn  4688  rabsneu  4690  eusn  4691  tppreqb  4768  elpreqpr  4827  uniintsn  4945  iin0  5327  dfepfr  5639  epfrc  5640  dmopab3  5903  dm0rn0  5908  dm0rn0OLD  5909  rnopab3  5940  ssdmres  6006  iresn0n0  6050  imadisj  6076  args  6088  dffr3  6095  intirr  6112  dminxp  6173  dfrel3  6192  coeq0  6252  snres0  6296  sspred  6308  dffr4  6318  frpomin2  6339  frpoind  6340  cbviotavw  6497  fntpg  6593  fncnv  6606  mptfnf  6667  sbcfng  6699  f0rn0  6760  dff1o4  6826  dffv4  6875  tz6.12c  6900  fvun2  6970  fnreseql  7040  funopdmsn  7147  riota1  7391  riota2df  7393  riotaeqimp  7396  fnbrovb  7464  ovid  7554  ov  7557  ovg  7578  ovima0  7593  opiota  8056  frrlem13  8297  tz7.49c  8435  sucprcreg  9578  sucprcregOLD  9579  zfregfr  9583  inf3lem2  9608  zfregs2  9712  frind  9732  rankxpsuc  9864  scott0b  9876  scott0bsOLD  9884  cplem1OLD  9890  cfslb2n  10270  fin23lem26  10327  dfacfin7  10401  axdc3lem4  10455  zorn2lem7  10504  alephom  10594  fpwwe2  10652  recmulnq  10973  recexsr  11116  map2psrpr  11119  renegcli  11543  addeq0  11661  elznn0  12630  xrsupss  13361  xrinfmss  13362  prinfzo0  13754  seqf1olem1  14105  seqf1olem2  14106  sqeqori  14278  hashrabsn1  14438  hashprb  14461  hashprdifel  14462  hashbclem  14517  hash2pwpr  14541  f1oun2prg  14988  modfsummods  15880  cshwrepswhash1  17194  ismgmid  18758  smndex2dnrinv  19027  oppgid  19483  lsmdisjr  19811  gexex  19980  gsumxp2  20107  dprd0  20160  oppr1  20491  opprunit  20518  isdrng4  20902  isdrng3lem1  20914  ssdifidlprm  21549  zringndrg  21681  gsummoncoe1  22533  mat0dimcrng  22692  iinopn  23127  elcls  23298  ordthaus  23609  hauscmplem  23631  regr1lem2  23966  metdseq0  25081  minveclem1  25652  minveclem3b  25656  volun  25773  dyaddisj  25824  vieta1  26544  logeftb  26820  birthdaylem1  27188  dmgmaddn0  27259  gausslemma2d  27610  lgseisenlem1  27611  2lgslem4  27642  rpvmasum  27762  ltssolem1  27911  noinfbnd2lem1  27966  madeval2  28098  made0  28128  axsegconlem6  29379  edg0iedg0  29512  numedglnl  29601  ushgredgedg  29689  ushgredgedgloop  29691  uhgr0v0e  29698  usgr1v0edg  29717  usgrexmpllem  29720  usgr1v0e  29786  nbuhgr2vtx1edgblem  29811  uvtx01vtx  29857  prcliscplgr  29874  cusgr0v  29888  vtxdg0e  29934  1loopgrvd2  29963  finsumvtxdg2ssteplem4  30008  finsumvtxdg2size  30010  isrgr  30019  fusgrregdegfi  30029  wspn0  30392  2wlkdlem8  30401  3wlkdlem8  30647  uhgr3cyclexlem  30661  1to2vfriswmgr  30759  1to3vfriswmgr  30760  frgrregorufr0  30804  frgrreg  30874  frgrregord013  30875  ex-ceil  30928  nmlno0lem  31274  minvecolem1  31355  hvsubeq0i  31544  hvsubaddi  31547  pjoc2i  31919  pjoml3i  32067  cmbr3i  32081  pjss2i  32161  hosubeq0i  32307  dmadjrnb  32387  nmlnop0iALT  32476  nmopcoadj0i  32584  stm1ri  32725  jplem2  32750  atoml2i  32864  chirredlem1  32871  cdj3lem3  32919  difininv  32992  disjnf  33043  disjpreima  33057  disjunsn  33067  f1od2  33190  wrdt2ind  33395  isunit2  33679  lsmsnorb2  33825  fldext2chn  34238  zrhchr  34484  ddemeas  34747  braew  34753  aean  34755  eulerpartlemgh  34889  ballotlemfp1  35003  repr0  35119  hgt750lem2  35160  bnj1143  35299  nummin  35598  scott0bOLD  35634  acycgr0v  35727  prclisacycgr  35730  cvmsss2  35853  cvmlift2lem13  35894  elrn3  36341  rankeq1o  36751  hfun  36758  bj-disj2r  37772  bj-sscon  37773  bj-0int  37851  bj-imdirco  37942  bj-pinftynminfty  37979  finxpreclem4  38148  nlpineqsn  38162  curunc  38356  tan2h  38366  poimirlem13  38382  poimirlem14  38383  poimirlem21  38390  poimirlem22  38391  asindmre  38452  totbndbnd  38539  rngosn3  38674  scott0f  38917  n0el2  39083  dfrel5  39094  dfrel6  39095  redundeq1  39461  dmqscoelseq  39494  dfeldisj5  39561  atbase  40162  llnbase  40382  lplnbase  40407  lvolbase  40451  lhpbase  40871  cdlemg31b0N  41567  cdlemg31b0a  41568  cdlemh  41690  sticksstones16  43028  sticksstones21  43033  unitscyglem3  43063  onsupmaxb  44080  iunrelexp0  44542  frege120  44823  clsk1indlem4  44884  gneispace  44974  undisjrab  45130  zfregs2VD  45663  dvnprod  46777  fnresfnco  47929  aiotavb  47978  afvpcfv0  48034  aovpcov0  48078  aov0ov0  48081  aovov0bi  48084  fnotaovb  48086  funressndmafv2rn  48111  fmtnoprmfac1lem  48467  lighneallem2  48509  stgrvtx0  48878  isubgr3stgrlem6  48887  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  snlindsntor  49401  rrx2pnedifcoorneorr  49647  itschlc0xyqsol1  49696  2itscp  49711  resinsn  49798  resinsnALT  49799  opndisj  49829  istermc  50400  lanrcl  50547  ranrcl  50548