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 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  eqeq12i  2778  eqabb  2899  neeq1i  3019  dfss2  4093  ineqcom  4106  dfss7  4147  ssequn2  4186  dfss4  4213  inssdif0  4321  rabeq0w  4336  rabeq0  4337  disj  4402  undisj1  4414  undisj2  4415  undif  4437  undifr  4438  rabeqsn  4624  reusn  4684  rabsneu  4686  eusn  4687  tppreqb  4764  elpreqpr  4821  uniintsn  4944  iin0  5323  dfepfr  5634  epfrc  5635  dmopab3  5901  dm0rn0  5906  dm0rn0OLD  5907  rnopab3  5938  ssdmres  6005  iresn0n0  6047  imadisj  6078  args  6091  dffr3  6098  intirr  6113  dminxp  6173  dfrel3  6194  coeq0  6259  snres0  6303  sspred  6315  dffr4  6325  frpomin2  6346  frpoind  6347  cbviotavw  6504  fntpg  6603  fncnv  6616  mptfnf  6677  sbcfng  6709  f0rn0  6770  dff1o4  6836  dffv4  6885  tz6.12c  6910  fvun2  6980  fnreseql  7050  funopdmsn  7157  riota1  7400  riota2df  7402  riotaeqimp  7405  fnbrovb  7473  ovid  7563  ov  7566  ovg  7587  ovima0  7602  mpt3fvd  7690  opiota  8072  f1od2  8112  frrlem13  8321  tz7.49c  8461  sucprcreg  9605  sucprcregOLD  9606  zfregfr  9610  inf3lem2  9635  zfregs2  9739  frind  9759  rankxpsuc  9904  hfunOLD  9924  scott0b  9942  scott0bsOLD  9950  cplem1OLD  9956  cfslb2n  10351  fin23lem26  10408  dfacfin7  10482  axdc3lem4  10536  zorn2lem7  10585  alephom  10675  fpwwe2  10733  recmulnq  11054  recexsr  11197  map2psrpr  11200  renegcli  11624  addeq0  11744  elznn0  12713  xrsupss  13444  xrinfmss  13445  prinfzo0  13838  seqf1olem1  14189  seqf1olem2  14190  sqeqori  14363  hashrabsn1  14523  hashprb  14546  hashprdifel  14547  hashbclem  14602  hash2pwpr  14626  f1oun2prg  15075  modfsummods  15967  cshwrepswhash1  17287  ismgmid  18852  smndex2dnrinv  19121  oppgid  19577  lsmdisjr  19905  gexex  20074  gsumxp2  20201  dprd0  20254  oppr1  20587  opprunit  20614  isdrng4  20999  isdrng3lem1  21012  ssdifidlprm  21649  zringndrg  21781  gsummoncoe1  22633  mat0dimcrng  22792  iinopn  23227  elcls  23398  ordthaus  23709  hauscmplem  23731  regr1lem2  24066  metdseq0  25181  minveclem1  25752  minveclem3b  25756  volun  25873  dyaddisj  25924  vieta1  26642  logeftb  26918  birthdaylem1  27286  dmgmaddn0  27357  gausslemma2d  27708  lgseisenlem1  27709  2lgslem4  27740  rpvmasum  27860  ltssolem1  28039  noinfbnd2lem1  28094  madeval2  28226  made0  28256  axsegconlem6  29507  edg0iedg0  29640  numedglnl  29729  ushgredgedg  29817  ushgredgedgloop  29819  uhgr0v0e  29826  usgr1v0edg  29845  usgrexmpllem  29848  usgr1v0e  29914  nbuhgr2vtx1edgblem  29939  uvtx01vtx  29985  prcliscplgr  30002  cusgr0v  30016  vtxdg0e  30062  1loopgrvd2  30091  finsumvtxdg2ssteplem4  30136  finsumvtxdg2size  30138  isrgr  30147  fusgrregdegfi  30157  wspn0  30520  2wlkdlem8  30529  3wlkdlem8  30775  uhgr3cyclexlem  30789  1to2vfriswmgr  30887  1to3vfriswmgr  30888  frgrregorufr0  30932  frgrreg  31002  frgrregord013  31003  ex-ceil  31056  nmlno0lem  31402  minvecolem1  31483  hvsubeq0i  31672  hvsubaddi  31675  pjoc2i  32047  pjoml3i  32195  cmbr3i  32209  pjss2i  32289  hosubeq0i  32435  dmadjrnb  32515  nmlnop0iALT  32604  nmopcoadj0i  32712  stm1ri  32853  jplem2  32878  atoml2i  32992  chirredlem1  32999  cdj3lem3  33047  difininv  33162  disjnf  33213  disjpreima  33227  disjunsn  33237  wrdt2ind  33564  isunit2  33848  lsmsnorb2  33995  fldext2chn  34408  zrhchr  34654  ddemeas  34917  braew  34923  aean  34925  eulerpartlemgh  35058  ballotlemfp1  35172  repr0  35288  hgt750lem2  35329  bnj1143  35468  nummin  35776  scott0bOLD  35807  acycgr0v  35991  prclisacycgr  35994  cvmsss2  36127  cvmlift2lem13  36168  elrn3  36621  rankeq1o  37026  bj-disj2r  38035  bj-sscon  38036  bj-dfrel3  38059  bj-dfrel4v  38061  bj-dfrel2  38062  bj-coi1  38067  bj-0int  38128  bj-imdirco  38218  bj-pinftynminfty  38255  finxpreclem4  38424  nlpineqsn  38438  curunc  38632  tan2h  38642  poimirlem13  38658  poimirlem14  38659  poimirlem21  38666  poimirlem22  38667  asindmre  38728  totbndbnd  38830  rngosn3  38965  scott0f  39208  n0el2  39374  dfrel5  39385  dfrel6  39386  redundeq1  39752  dmqscoelseq  39785  dfeldisj5  39852  atbase  40453  llnbase  40673  lplnbase  40698  lvolbase  40742  lhpbase  41162  cdlemg31b0N  41858  cdlemg31b0a  41859  cdlemh  41981  sticksstones16  43319  sticksstones21  43324  unitscyglem3  43354  onsupmaxb  44348  iunrelexp0  44809  frege120  45090  clsk1indlem4  45151  gneispace  45241  undisjrab  45397  zfregs2VD  45930  dvnprod  47066  fnresfnco  48218  aiotavb  48267  afvpcfv0  48323  aovpcov0  48367  aov0ov0  48370  aovov0bi  48373  fnotaovb  48375  funressndmafv2rn  48400  fmtnoprmfac1lem  48756  lighneallem2  48798  stgrvtx0  49167  isubgr3stgrlem6  49176  pgnbgreunbgrlem2lem1  49319  pgnbgreunbgrlem2lem2  49320  pgnbgreunbgrlem2lem3  49321  snlindsntor  49690  rrx2pnedifcoorneorr  49937  itschlc0xyqsol1  49985  2itscp  50000  resinsn  50092  resinsnALT  50093  opndisj  50124  istermc  50716  lanrcl  50911  ranrcl  50912