MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq2i Unicode version

Theorem eqeq2i 2293
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqeq2i.1  |-  A  =  B
Assertion
Ref Expression
eqeq2i  |-  ( C  =  A  <->  C  =  B )

Proof of Theorem eqeq2i
StepHypRef Expression
1 eqeq2i.1 . 2  |-  A  =  B
2 eqeq2 2292 . 2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
31, 2ax-mp 8 1  |-  ( C  =  A  <->  C  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623
This theorem is referenced by:  eqtri  2303  rabid2  2717  dfss2  3169  equncom  3320  ssunpr  3776  sspr  3777  sstp  3778  preq12b  3788  preqsn  3792  opeqpr  4263  wefrc  4387  orddif  4486  onuninsuci  4631  dfrel4v  5125  dfiota2  5220  funopg  5286  funimaexg  5329  dffn5f  5577  fnressn  5705  fressnfv  5707  fvresex  5762  fnov  5952  elxp6  6151  tpossym  6266  opiota  6290  qsid  6725  mapsncnv  6814  ixpsnf1o  6856  card1  7601  pm54.43lem  7632  cf0  7877  sdom2en01  7928  cardeq0  8174  enqbreq2  8544  addcompr  8645  mulcompr  8647  axrrecex  8785  negeq0  9101  muleqadd  9412  crne0  9739  dfnn3  9760  xmulneg1  10589  hasheq0  11353  hashbc  11391  hashf1lem2  11394  cjne0  11648  sqr00  11749  sqrmsq2i  11871  fsump1i  12232  absefib  12478  efieq1re  12479  xpccatid  13962  isnsg4  14660  2ndcctbss  17181  ptcnp  17316  ovolgelb  18839  ioorinv  18931  rolle  19337  plymul0or  19661  reeff1o  19823  sineq0  19889  coseq1  19890  1cubr  20138  atandm2  20173  atandm3  20174  efrlim  20264  isppw  20352  ppiub  20443  lgsdinn0  20579  m1lgs  20601  isgrpo  20863  vci  21104  chnlei  22064  h1de2ctlem  22134  cmcmlem  22170  cmcm2i  22172  cmbr2i  22175  osumcor2i  22223  pjss2i  22259  ho01i  22408  nmop0h  22571  pjclem1  22775  jplem1  22848  atabs2i  22982  rabid2f  23135  preqsnd  23194  dfrel4  23204  subfacp1lem6  23716  trpredmintr  24234  brdomain  24472  brrange  24473  brimg  24476  brapply  24477  brsuccf  24480  brfullfun  24486  brrestrict  24487  bpoly2  24792  bpoly3  24793  bpoly4  24794  rankeq1o  24801  dffn5a  25130  islatalg  25183  com2i  25416  vri  25492  usptop  25550  algi  25727  dedi  25737  cati  25755  opropabco  26389  fdc  26455  isdrngo1  26587  smprngopr  26677  mzpcompact2lem  26829  eldioph4b  26894  2nn0ind  27030  islmodfg  27167  elnev  27638  bnj168  28758  bnj927  28800  bnj543  28925  bnj970  28979  cdleme25cv  30547  cdlemk35  31101  dicval2  31369  dicopelval2  31371  dicelval2N  31372  hdmap1fval  31987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator