Theorem eqeq1i 2766

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 2765	. 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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  eqeq12i  2779  eqabb  2900  neeq1i  3020  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  5324  dfepfr  5635  epfrc  5636  dmopab3  5901  dm0rn0  5906  dm0rn0OLD  5907  rnopab3  5938  ssdmres  6004  iresn0n0  6046  imadisj  6077  args  6090  dffr3  6097  intirr  6112  dminxp  6172  dfrel3  6191  coeq0  6256  snres0  6300  sspred  6312  dffr4  6322  frpomin2  6343  frpoind  6344  cbviotavw  6501  fntpg  6598  fncnv  6611  mptfnf  6672  sbcfng  6704  f0rn0  6765  dff1o4  6831  dffv4  6880  tz6.12c  6905  fvun2  6975  fnreseql  7045  funopdmsn  7152  riota1  7396  riota2df  7398  riotaeqimp  7401  fnbrovb  7469  ovid  7559  ov  7562  ovg  7583  ovima0  7598  mpt3fvd  7686  opiota  8068  frrlem13  8309  tz7.49c  8449  sucprcreg  9593  sucprcregOLD  9594  zfregfr  9598  inf3lem2  9623  zfregs2  9727  frind  9747  rankxpsuc  9892  hfunOLD  9912  scott0b  9930  scott0bsOLD  9938  cplem1OLD  9944  cfslb2n  10339  fin23lem26  10396  dfacfin7  10470  axdc3lem4  10524  zorn2lem7  10573  alephom  10663  fpwwe2  10721  recmulnq  11042  recexsr  11185  map2psrpr  11188  renegcli  11612  addeq0  11732  elznn0  12701  xrsupss  13432  xrinfmss  13433  prinfzo0  13826  seqf1olem1  14177  seqf1olem2  14178  sqeqori  14351  hashrabsn1  14511  hashprb  14534  hashprdifel  14535  hashbclem  14590  hash2pwpr  14614  f1oun2prg  15061  modfsummods  15953  cshwrepswhash1  17273  ismgmid  18838  smndex2dnrinv  19107  oppgid  19563  lsmdisjr  19891  gexex  20060  gsumxp2  20187  dprd0  20240  oppr1  20573  opprunit  20600  isdrng4  20985  isdrng3lem1  20998  ssdifidlprm  21635  zringndrg  21767  gsummoncoe1  22619  mat0dimcrng  22778  iinopn  23213  elcls  23384  ordthaus  23695  hauscmplem  23717  regr1lem2  24052  metdseq0  25167  minveclem1  25738  minveclem3b  25742  volun  25859  dyaddisj  25910  vieta1  26628  logeftb  26904  birthdaylem1  27272  dmgmaddn0  27343  gausslemma2d  27694  lgseisenlem1  27695  2lgslem4  27726  rpvmasum  27846  ltssolem1  28025  noinfbnd2lem1  28080  madeval2  28212  made0  28242  axsegconlem6  29493  edg0iedg0  29626  numedglnl  29715  ushgredgedg  29803  ushgredgedgloop  29805  uhgr0v0e  29812  usgr1v0edg  29831  usgrexmpllem  29834  usgr1v0e  29900  nbuhgr2vtx1edgblem  29925  uvtx01vtx  29971  prcliscplgr  29988  cusgr0v  30002  vtxdg0e  30048  1loopgrvd2  30077  finsumvtxdg2ssteplem4  30122  finsumvtxdg2size  30124  isrgr  30133  fusgrregdegfi  30143  wspn0  30506  2wlkdlem8  30515  3wlkdlem8  30761  uhgr3cyclexlem  30775  1to2vfriswmgr  30873  1to3vfriswmgr  30874  frgrregorufr0  30918  frgrreg  30988  frgrregord013  30989  ex-ceil  31042  nmlno0lem  31388  minvecolem1  31469  hvsubeq0i  31658  hvsubaddi  31661  pjoc2i  32033  pjoml3i  32181  cmbr3i  32195  pjss2i  32275  hosubeq0i  32421  dmadjrnb  32501  nmlnop0iALT  32590  nmopcoadj0i  32698  stm1ri  32839  jplem2  32864  atoml2i  32978  chirredlem1  32985  cdj3lem3  33033  difininv  33106  disjnf  33157  disjpreima  33171  disjunsn  33181  f1od2  33304  wrdt2ind  33509  isunit2  33793  lsmsnorb2  33940  fldext2chn  34353  zrhchr  34599  ddemeas  34862  braew  34868  aean  34870  eulerpartlemgh  35003  ballotlemfp1  35117  repr0  35233  hgt750lem2  35274  bnj1143  35413  nummin  35711  scott0bOLD  35739  acycgr0v  35892  prclisacycgr  35895  cvmsss2  36018  cvmlift2lem13  36059  elrn3  36506  rankeq1o  36912  bj-disj2r  37921  bj-sscon  37922  bj-0int  38002  bj-imdirco  38091  bj-pinftynminfty  38128  finxpreclem4  38297  nlpineqsn  38311  curunc  38505  tan2h  38515  poimirlem13  38531  poimirlem14  38532  poimirlem21  38539  poimirlem22  38540  asindmre  38601  totbndbnd  38703  rngosn3  38838  scott0f  39081  n0el2  39247  dfrel5  39258  dfrel6  39259  redundeq1  39625  dmqscoelseq  39658  dfeldisj5  39725  atbase  40326  llnbase  40546  lplnbase  40571  lvolbase  40615  lhpbase  41035  cdlemg31b0N  41731  cdlemg31b0a  41732  cdlemh  41854  sticksstones16  43192  sticksstones21  43197  unitscyglem3  43227  onsupmaxb  44225  iunrelexp0  44687  frege120  44968  clsk1indlem4  45029  gneispace  45119  undisjrab  45275  zfregs2VD  45808  dvnprod  46928  fnresfnco  48080  aiotavb  48129  afvpcfv0  48185  aovpcov0  48229  aov0ov0  48232  aovov0bi  48235  fnotaovb  48237  funressndmafv2rn  48262  fmtnoprmfac1lem  48618  lighneallem2  48660  stgrvtx0  49029  isubgr3stgrlem6  49038  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  snlindsntor  49552  rrx2pnedifcoorneorr  49798  itschlc0xyqsol1  49847  2itscp  49862  resinsn  49949  resinsnALT  49950  opndisj  49980  istermc  50551  lanrcl  50698  ranrcl  50699