Theorem eqeq1i 2768

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 2767	. 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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqeq12i  2781  eqabb  2903  neeq1i  3023  dfss2  4097  ineqcom  4110  dfss7  4151  ssequn2  4190  dfss4  4217  inssdif0  4325  rabeq0w  4340  rabeq0  4341  disj  4406  undisj1  4418  undisj2  4419  undif  4441  undifr  4442  rabeqsn  4629  reusn  4690  rabsneu  4692  eusn  4693  tppreqb  4770  elpreqpr  4827  uniintsn  4950  iin0  5331  dfepfr  5642  epfrc  5643  dmopab3  5913  dm0rn0  5918  dm0rn0OLD  5919  rnopab3  5950  ssdmres  6021  iresn0n0  6064  imadisj  6095  args  6108  dffr3  6115  intirr  6130  dminxp  6190  dfrel3  6211  coeq0  6276  snres0  6327  sspred  6339  dffr4  6349  frpomin2  6370  frpoind  6371  cbviotavw  6528  fntpg  6630  fncnv  6643  mptfnf  6704  sbcfng  6736  f0rn0  6797  dff1o4  6863  dffv4  6913  tz6.12c  6938  fvun2  7008  fnreseql  7078  funopdmsn  7186  riota1  7429  riota2df  7431  riotaeqimp  7434  fnbrovb  7502  ovid  7593  ov  7596  ovg  7617  ovima0  7632  mpt3fvd  7720  opiota  8105  f1od2  8145  frrlem13  8354  tz7.49c  8494  sucprcreg  9637  sucprcregOLD  9638  zfregfr  9642  inf3lem2  9667  zfregs2  9771  frind  9791  rankxpsuc  9936  hfunOLD  9956  scott0b  9974  scott0bsOLD  9982  cplem1OLD  9988  cfslb2n  10385  fin23lem26  10442  dfacfin7  10516  axdc3lem4  10570  zorn2lem7  10619  alephom  10709  fpwwe2  10767  recmulnq  11088  recexsr  11231  map2psrpr  11234  renegcli  11658  addeq0  11778  elznn0  12748  xrsupss  13479  xrinfmss  13480  prinfzo0  13873  seqf1olem1  14224  seqf1olem2  14225  sqeqori  14399  hashrabsn1  14559  hashprb  14582  hashprdifel  14583  hashbclem  14638  hash2pwpr  14662  f1oun2prg  15111  modfsummods  16004  cshwrepswhash1  17324  ismgmid  18895  smndex2dnrinv  19164  oppgid  19621  lsmdisjr  19949  gexex  20118  gsumxp2  20245  dprd0  20298  oppr1  20631  opprunit  20658  isdrng4  21043  isdrng3lem1  21056  ssdifidlprm  21693  zringndrg  21829  gsummoncoe1  22681  mat0dimcrng  22840  iinopn  23275  elcls  23446  ordthaus  23757  hauscmplem  23779  regr1lem2  24114  metdseq0  25229  minveclem1  25800  minveclem3b  25804  volun  25921  dyaddisj  25972  vieta1  26690  logeftb  26968  birthdaylem1  27336  dmgmaddn0  27407  gausslemma2d  27758  lgseisenlem1  27759  2lgslem4  27790  rpvmasum  27910  ltssolem1  28089  noinfbnd2lem1  28144  madeval2  28276  made0  28306  axsegconlem6  29557  edg0iedg0  29690  numedglnl  29779  ushgredgedg  29867  ushgredgedgloop  29869  uhgr0v0e  29876  usgr1v0edg  29895  usgrexmpllem  29898  usgr1v0e  29964  nbuhgr2vtx1edgblem  29989  uvtx01vtx  30035  prcliscplgr  30052  cusgr0v  30066  vtxdg0e  30112  1loopgrvd2  30141  finsumvtxdg2ssteplem4  30186  finsumvtxdg2size  30188  isrgr  30197  fusgrregdegfi  30207  wspn0  30570  2wlkdlem8  30579  3wlkdlem8  30825  uhgr3cyclexlem  30839  1to2vfriswmgr  30937  1to3vfriswmgr  30938  frgrregorufr0  30982  frgrreg  31052  frgrregord013  31053  ex-ceil  31106  nmlno0lem  31452  minvecolem1  31533  hvsubeq0i  31722  hvsubaddi  31725  pjoc2i  32097  pjoml3i  32245  cmbr3i  32259  pjss2i  32339  hosubeq0i  32485  dmadjrnb  32565  nmlnop0iALT  32654  nmopcoadj0i  32762  stm1ri  32903  jplem2  32928  atoml2i  33042  chirredlem1  33049  cdj3lem3  33097  difininv  33212  disjnf  33262  disjpreima  33276  disjunsn  33286  wrdt2ind  33612  isunit2  33899  lsmsnorb2  34051  fldext2chn  34471  zrhchr  34717  ddemeas  34980  braew  34986  aean  34988  eulerpartlemgh  35121  ballotlemfp1  35235  repr0  35351  hgt750lem2  35392  bnj1143  35531  nummin  35847  scott0bOLD  35876  acycgr0v  36111  prclisacycgr  36114  cvmsss2  36247  cvmlift2lem13  36288  elrn3  36742  rankeq1o  37147  bj-disj2r  38156  bj-sscon  38157  bj-resssxp  38183  bj-dfrel4v  38190  bj-dfrel2  38191  bj-coi1  38203  bj-0int  38292  bj-imdirco  38379  bj-pinftynminfty  38416  finxpreclem4  38585  nlpineqsn  38599  curunc  38793  tan2h  38803  poimirlem13  38819  poimirlem14  38820  poimirlem21  38827  poimirlem22  38828  asindmre  38889  totbndbnd  38989  rngosn3  39124  scott0f  39367  n0el2  39533  dfrel5  39544  dfrel6  39545  redundeq1  39911  dmqscoelseq  39944  dfeldisj5  40011  atbase  40612  llnbase  40832  lplnbase  40857  lvolbase  40901  lhpbase  41321  cdlemg31b0N  42017  cdlemg31b0a  42018  cdlemh  42140  sticksstones16  43478  sticksstones21  43483  unitscyglem3  43513  onsupmaxb  44502  iunrelexp0  44963  frege120  45244  clsk1indlem4  45305  gneispace  45395  undisjrab  45551  zfregs2VD  46083  dvnprod  47232  fnresfnco  48384  aiotavb  48433  afvpcfv0  48489  aovpcov0  48533  aov0ov0  48536  aovov0bi  48539  fnotaovb  48541  funressndmafv2rn  48566  fmtnoprmfac1lem  48922  lighneallem2  48964  stgrvtx0  49333  isubgr3stgrlem6  49342  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  snlindsntor  49914  rrx2pnedifcoorneorr  50161  itschlc0xyqsol1  50209  2itscp  50224  resinsn  50316  resinsnALT  50317  opndisj  50348  istermc  50940  lanrcl  51135  ranrcl  51136