Theorem eqeq1i 2767

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 2766	. 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 2734

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

This theorem is used by:  eqeq12i  2780  eqabb  2901  neeq1i  3021  dfss2  3920  ssequn2  4138  ineqcom  4159  dfss7  4200  dfss4  4218  inssdif0  4325  rabeq0w  4340  rabeq0  4341  disj  4406  undisj1  4418  undisj2  4419  undif  4441  undifr  4442  rabeqsn  4631  reusn  4691  rabsneu  4693  eusn  4694  tppreqb  4771  elpreqpr  4830  uniintsn  4948  iin0  5331  dfepfr  5643  epfrc  5644  dmopab3  5907  dm0rn0  5912  dm0rn0OLD  5913  rnopab3  5944  ssdmres  6010  iresn0n0  6054  imadisj  6080  args  6092  dffr3  6099  intirr  6116  dminxp  6177  dfrel3  6196  coeq0  6256  snres0  6300  sspred  6312  dffr4  6322  frpomin2  6343  frpoind  6344  cbviotavw  6501  fntpg  6597  fncnv  6610  mptfnf  6671  sbcfng  6703  f0rn0  6764  dff1o4  6830  dffv4  6879  tz6.12c  6904  fvun2  6974  fnreseql  7044  funopdmsn  7150  riota1  7394  riota2df  7396  riotaeqimp  7399  fnbrovb  7467  ovid  7557  ov  7560  ovg  7581  ovima0  7596  opiota  8059  frrlem13  8300  tz7.49c  8438  sucprcreg  9581  sucprcregOLD  9582  zfregfr  9586  inf3lem2  9611  zfregs2  9715  frind  9735  rankxpsuc  9867  scott0b  9879  scott0bsOLD  9887  cplem1OLD  9893  cfslb2n  10273  fin23lem26  10330  dfacfin7  10404  axdc3lem4  10458  zorn2lem7  10507  alephom  10597  fpwwe2  10655  recmulnq  10976  recexsr  11119  map2psrpr  11122  renegcli  11546  addeq0  11664  elznn0  12633  xrsupss  13363  xrinfmss  13364  prinfzo0  13756  seqf1olem1  14107  seqf1olem2  14108  sqeqori  14280  hashrabsn1  14440  hashprb  14463  hashprdifel  14464  hashbclem  14519  hash2pwpr  14543  f1oun2prg  14990  modfsummods  15882  cshwrepswhash1  17198  ismgmid  18762  smndex2dnrinv  19031  oppgid  19487  lsmdisjr  19815  gexex  19984  gsumxp2  20111  dprd0  20164  oppr1  20495  opprunit  20522  isdrng4  20906  isdrng3lem1  20918  ssdifidlprm  21553  zringndrg  21685  gsummoncoe1  22537  mat0dimcrng  22696  iinopn  23131  elcls  23302  ordthaus  23613  hauscmplem  23635  regr1lem2  23970  metdseq0  25085  minveclem1  25656  minveclem3b  25660  volun  25777  dyaddisj  25828  vieta1  26546  logeftb  26821  birthdaylem1  27189  dmgmaddn0  27260  gausslemma2d  27611  lgseisenlem1  27612  2lgslem4  27643  rpvmasum  27763  ltssolem1  27912  noinfbnd2lem1  27967  madeval2  28099  made0  28129  axsegconlem6  29380  edg0iedg0  29513  numedglnl  29602  ushgredgedg  29690  ushgredgedgloop  29692  uhgr0v0e  29699  usgr1v0edg  29718  usgrexmpllem  29721  usgr1v0e  29787  nbuhgr2vtx1edgblem  29812  uvtx01vtx  29858  prcliscplgr  29875  cusgr0v  29889  vtxdg0e  29935  1loopgrvd2  29964  finsumvtxdg2ssteplem4  30009  finsumvtxdg2size  30011  isrgr  30020  fusgrregdegfi  30030  wspn0  30393  2wlkdlem8  30402  3wlkdlem8  30648  uhgr3cyclexlem  30662  1to2vfriswmgr  30760  1to3vfriswmgr  30761  frgrregorufr0  30805  frgrreg  30875  frgrregord013  30876  ex-ceil  30929  nmlno0lem  31275  minvecolem1  31356  hvsubeq0i  31545  hvsubaddi  31548  pjoc2i  31920  pjoml3i  32068  cmbr3i  32082  pjss2i  32162  hosubeq0i  32308  dmadjrnb  32388  nmlnop0iALT  32477  nmopcoadj0i  32585  stm1ri  32726  jplem2  32751  atoml2i  32865  chirredlem1  32872  cdj3lem3  32920  difininv  32993  disjnf  33045  disjpreima  33059  disjunsn  33069  f1od2  33192  wrdt2ind  33397  isunit2  33681  lsmsnorb2  33827  fldext2chn  34240  zrhchr  34486  ddemeas  34749  braew  34755  aean  34757  eulerpartlemgh  34891  ballotlemfp1  35005  repr0  35121  hgt750lem2  35162  bnj1143  35301  nummin  35600  scott0bOLD  35636  acycgr0v  35729  prclisacycgr  35732  cvmsss2  35855  cvmlift2lem13  35896  elrn3  36343  rankeq1o  36753  hfun  36760  bj-disj2r  37774  bj-sscon  37775  bj-0int  37853  bj-imdirco  37944  bj-pinftynminfty  37981  finxpreclem4  38150  nlpineqsn  38164  curunc  38358  tan2h  38368  poimirlem13  38384  poimirlem14  38385  poimirlem21  38392  poimirlem22  38393  asindmre  38454  totbndbnd  38541  rngosn3  38676  scott0f  38919  n0el2  39085  dfrel5  39096  dfrel6  39097  redundeq1  39463  dmqscoelseq  39496  dfeldisj5  39563  atbase  40164  llnbase  40384  lplnbase  40409  lvolbase  40453  lhpbase  40873  cdlemg31b0N  41569  cdlemg31b0a  41570  cdlemh  41692  sticksstones16  43030  sticksstones21  43035  unitscyglem3  43065  onsupmaxb  44082  iunrelexp0  44544  frege120  44825  clsk1indlem4  44886  gneispace  44976  undisjrab  45132  zfregs2VD  45665  dvnprod  46779  fnresfnco  47931  aiotavb  47980  afvpcfv0  48036  aovpcov0  48080  aov0ov0  48083  aovov0bi  48086  fnotaovb  48088  funressndmafv2rn  48113  fmtnoprmfac1lem  48469  lighneallem2  48511  stgrvtx0  48880  isubgr3stgrlem6  48889  pgnbgreunbgrlem2lem1  49032  pgnbgreunbgrlem2lem2  49033  pgnbgreunbgrlem2lem3  49034  snlindsntor  49403  rrx2pnedifcoorneorr  49649  itschlc0xyqsol1  49698  2itscp  49713  resinsn  49800  resinsnALT  49801  opndisj  49831  istermc  50402  lanrcl  50549  ranrcl  50550