Theorem eqeq1i 2770

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 2769	. 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 2156  ax-ext 2737

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

This theorem is used by:  eqeq12i  2783  eqabb  2904  neeq1i  3024  dfss2  3924  ssequn2  4142  ineqcom  4163  dfss7  4204  dfss4  4222  inssdif0  4329  rabeq0w  4344  rabeq0  4345  disj  4410  undisj1  4422  undisj2  4423  undif  4445  undifr  4446  rabeqsn  4635  reusn  4695  rabsneu  4697  eusn  4698  tppreqb  4775  elpreqpr  4834  uniintsn  4952  iin0  5335  dfepfr  5647  epfrc  5648  dmopab3  5911  dm0rn0  5916  dm0rn0OLD  5917  rnopab3  5948  ssdmres  6014  iresn0n0  6058  imadisj  6084  args  6096  dffr3  6103  intirr  6120  dminxp  6180  dfrel3  6199  coeq0  6259  snres0  6303  sspred  6315  dffr4  6325  frpomin2  6346  frpoind  6347  cbviotavw  6504  fntpg  6600  fncnv  6613  mptfnf  6674  sbcfng  6706  f0rn0  6767  dff1o4  6833  dffv4  6882  tz6.12c  6907  fvun2  6977  fnreseql  7047  funopdmsn  7153  riota1  7397  riota2df  7399  riotaeqimp  7402  fnbrovb  7470  ovid  7560  ov  7563  ovg  7584  ovima0  7599  opiota  8062  frrlem13  8301  tz7.49c  8439  sucprcreg  9575  sucprcregOLD  9576  zfregfr  9580  inf3lem2  9605  zfregs2  9709  frind  9729  rankxpsuc  9861  scott0b  9873  scott0bsOLD  9881  cplem1OLD  9887  cfslb2n  10267  fin23lem26  10324  dfacfin7  10398  axdc3lem4  10452  zorn2lem7  10501  alephom  10585  fpwwe2  10643  recmulnq  10964  recexsr  11107  map2psrpr  11110  renegcli  11534  addeq0  11652  elznn0  12621  xrsupss  13351  xrinfmss  13352  prinfzo0  13744  seqf1olem1  14095  seqf1olem2  14096  sqeqori  14268  hashrabsn1  14428  hashprb  14451  hashprdifel  14452  hashbclem  14507  hash2pwpr  14531  f1oun2prg  14978  modfsummods  15868  cshwrepswhash1  17184  ismgmid  18748  smndex2dnrinv  19014  oppgid  19470  lsmdisjr  19798  gexex  19967  gsumxp2  20094  dprd0  20147  oppr1  20478  opprunit  20505  isdrng4  20889  isdrng3lem1  20901  ssdifidlprm  21536  zringndrg  21668  gsummoncoe1  22518  mat0dimcrng  22677  iinopn  23109  elcls  23280  ordthaus  23591  hauscmplem  23613  regr1lem2  23948  metdseq0  25063  minveclem1  25634  minveclem3b  25638  volun  25755  dyaddisj  25806  vieta1  26524  logeftb  26799  birthdaylem1  27167  dmgmaddn0  27238  gausslemma2d  27589  lgseisenlem1  27590  2lgslem4  27621  rpvmasum  27741  ltssolem1  27890  noinfbnd2lem1  27945  madeval2  28077  made0  28107  axsegconlem6  29327  edg0iedg0  29460  numedglnl  29549  ushgredgedg  29637  ushgredgedgloop  29639  uhgr0v0e  29646  usgr1v0edg  29665  usgrexmpllem  29668  usgr1v0e  29734  nbuhgr2vtx1edgblem  29759  uvtx01vtx  29805  prcliscplgr  29822  cusgr0v  29836  vtxdg0e  29882  1loopgrvd2  29911  finsumvtxdg2ssteplem4  29956  finsumvtxdg2size  29958  isrgr  29967  fusgrregdegfi  29977  wspn0  30340  2wlkdlem8  30349  3wlkdlem8  30589  uhgr3cyclexlem  30603  1to2vfriswmgr  30701  1to3vfriswmgr  30702  frgrregorufr0  30746  frgrreg  30816  frgrregord013  30817  ex-ceil  30870  nmlno0lem  31216  minvecolem1  31297  hvsubeq0i  31486  hvsubaddi  31489  pjoc2i  31861  pjoml3i  32009  cmbr3i  32023  pjss2i  32103  hosubeq0i  32249  dmadjrnb  32329  nmlnop0iALT  32418  nmopcoadj0i  32526  stm1ri  32667  jplem2  32692  atoml2i  32806  chirredlem1  32813  cdj3lem3  32861  difininv  32934  disjnf  32986  disjpreima  33000  disjunsn  33010  f1od2  33134  wrdt2ind  33339  isunit2  33623  lsmsnorb2  33769  fldext2chn  34182  zrhchr  34428  ddemeas  34691  braew  34697  aean  34699  eulerpartlemgh  34833  ballotlemfp1  34947  repr0  35063  hgt750lem2  35104  bnj1143  35243  nummin  35542  scott0bOLD  35578  acycgr0v  35677  prclisacycgr  35680  cvmsss2  35803  cvmlift2lem13  35844  elrn3  36291  rankeq1o  36700  hfun  36707  bj-disj2r  37721  bj-sscon  37722  bj-0int  37800  bj-imdirco  37891  bj-pinftynminfty  37928  finxpreclem4  38097  nlpineqsn  38111  curunc  38310  tan2h  38320  poimirlem13  38341  poimirlem14  38342  poimirlem21  38349  poimirlem22  38350  asindmre  38411  totbndbnd  38498  rngosn3  38633  scott0f  38876  n0el2  39042  dfrel5  39053  dfrel6  39054  redundeq1  39420  dmqscoelseq  39453  dfeldisj5  39520  atbase  40121  llnbase  40341  lplnbase  40366  lvolbase  40410  lhpbase  40830  cdlemg31b0N  41526  cdlemg31b0a  41527  cdlemh  41649  sticksstones16  42987  sticksstones21  42992  unitscyglem3  43022  onsupmaxb  44024  iunrelexp0  44486  frege120  44767  clsk1indlem4  44828  gneispace  44918  undisjrab  45074  zfregs2VD  45607  dvnprod  46721  fnresfnco  47836  aiotavb  47885  afvpcfv0  47941  aovpcov0  47985  aov0ov0  47988  aovov0bi  47991  fnotaovb  47993  funressndmafv2rn  48018  fmtnoprmfac1lem  48374  lighneallem2  48416  stgrvtx0  48785  isubgr3stgrlem6  48794  pgnbgreunbgrlem2lem1  48937  pgnbgreunbgrlem2lem2  48938  pgnbgreunbgrlem2lem3  48939  snlindsntor  49308  rrx2pnedifcoorneorr  49554  itschlc0xyqsol1  49603  2itscp  49618  resinsn  49707  resinsnALT  49708  opndisj  49738  istermc  50309  lanrcl  50456  ranrcl  50457