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

Theorem eqeq1 2447
Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Assertion
Ref Expression
eqeq1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )

Proof of Theorem eqeq1
StepHypRef Expression
1 id 22 . 2  |-  ( A  =  B  ->  A  =  B )
21eqeq1d 2445 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  eqeq1i  2450  eqeq2OLD  2459  eqeq12  2462  eqtr  2469  eqsb3lem  2562  clelab  2587  clelabOLD  2588  neeq1OLD  2725  pm13.18  2754  issetf  3100  sbhypf  3142  vtoclgft  3143  rexraleqim  3211  eqvincf  3213  pm13.183  3226  eueq  3257  mob  3267  euind  3272  reu2eqd  3282  reuind  3289  eqsbc3  3353  csbhypf  3439  uniiunlem  3573  snjust  4013  elprg  4030  elsncg  4037  rabrsn  4085  sneqrg  4184  preq12bg  4194  prel12g  4195  intab  4302  uniintsn  4309  dfiin2g  4348  disji2  4424  disjprg  4433  eusv1  4631  reusv2lem2  4639  reusv3  4645  reusv6OLD  4648  opthg  4712  copsexg  4722  copsexgOLD  4723  euotd  4738  otiunsndisj  4743  elopab  4745  solin  4813  elxpi  5005  opbrop  5069  relop  5143  ideqg  5144  elrnmpt  5239  elrnmpt1  5241  elrnmptg  5242  somin1  5393  cnveqb  5452  relcoi1  5526  funopg  5610  f0rn0  5760  fvelrnb  5905  fvmptg  5939  fndmin  5979  eldmrexrn  6022  foelrn  6035  foco2  6036  fmptco  6049  fmptsng  6077  fmptsnd  6078  eufnfv  6131  elabrex  6140  abrexco  6141  f1veqaeq  6153  isosolem  6228  f1oiso  6232  eusvobj2  6274  oprabid  6308  oprabv  6330  mpt2fun  6389  elrnmpt2g  6399  elrnmpt2  6400  elrnmpt2res  6401  ralrnmpt2  6402  ov3  6424  ov6g  6425  ovelrn  6436  caovcang  6461  caovcan  6464  snnex  6591  uniuni  6594  orduninsuc  6663  funcnvuni  6738  fun11iun  6745  f1oweALT  6769  opiota  6844  eloprabi  6847  frxp  6895  funsssuppss  6928  dftpos4  6976  tz7.44-2  7075  tz7.44-3  7076  oev  7166  oalimcl  7211  omlimcl  7229  odi  7230  omeu  7236  oeeui  7253  nneob  7303  omopth  7309  elqsg  7365  qsdisj  7390  qsel  7392  brecop  7406  eroveu  7408  erovlem  7409  elixpsn  7510  ixpsnf1o  7511  boxcutc  7514  2dom  7590  fundmen  7591  xpf1o  7681  nneneq  7702  fofinf1o  7803  elfi  7875  elfiun  7892  dffi3  7893  brwdom  7996  brwdom3  8011  unwdomg  8013  xpwdomg  8014  noinfep  8079  cantnfp1lem1  8100  cantnfp1lem3  8102  cantnflem1  8111  cantnfp1lem1OLD  8126  cantnfp1lem3OLD  8128  cantnfp1OLD  8129  cantnflem1OLD  8134  scott0  8307  carden2a  8350  cardiun  8366  pm54.43lem  8383  alephval3  8494  dfac5lem3  8509  dfac5lem4  8510  dfac2  8514  kmlem9  8541  kmlem12  8544  cardcf  8635  cfeq0  8639  cfsuc  8640  cff1  8641  cflim2  8646  cfss  8648  isfin5  8682  fin1a2lem11  8793  fin1a2lem13  8795  brdom7disj  8912  brdom6disj  8913  canthp1lem2  9034  canthp1  9035  tskuni  9164  gruina  9199  genpv  9380  genpelv  9381  addsrmo  9453  mulsrmo  9454  ltsosr  9474  ltresr  9520  axcnre  9544  axpre-lttri  9545  ltordlem  10085  ltord1  10086  fimaxre3  10499  supmul1  10515  supmullem1  10516  supmullem2  10517  supmul  10518  creur  10537  creui  10538  nn1m1nn  10563  elz  10873  nn0ind-raph  10971  xnegeq  11417  xmullem2  11468  xmulasslem  11488  fleqceilz  11963  fseqsupubi  12070  sqeqor  12264  nn0opth2  12334  hash1snb  12461  hash2prde  12498  hash2prd  12500  hash2pwpr  12501  brfi1uzind  12514  wrd2ind  12685  cshfn  12743  2cshwcshw  12775  scshwfzeqfzo  12776  shftfval  12885  sgnval  12903  sqrlem6  13063  summo  13521  fsum  13524  telfsumo  13598  infcvgaux1i  13650  infcvgaux2i  13651  mertenslem1  13675  mertenslem2  13676  mertens  13677  prodmo  13725  fprod  13730  ruclem12  13956  divalg  14043  ndvdssub  14047  sadcp1  14087  smupp1  14112  gcdval  14128  bezoutlem1  14158  bezoutlem3  14160  bezoutlem4  14161  bezout  14162  dvdsprime  14212  nprm  14213  dvdsprm  14222  coprm  14223  qnumval  14252  qdenval  14253  m1dvdsndvds  14307  reumodprminv  14311  pcval  14350  pceu  14352  pczpre  14353  pcdiv  14358  4sqlem2  14449  4sqlem4  14452  4sqlem12  14456  4sq  14464  vdwapval  14473  vdwapun  14474  vdwlem6  14486  cshwrepswhash1  14569  acsfn  15038  posi  15558  gsumval2a  15885  mgm2nsgrplem2  16016  mgm2nsgrplem3  16017  sgrp2nmndlem5  16026  mgmnsgrpex  16028  sgrpnmndex  16029  ghmf1  16274  conjnmzb  16280  orbsta  16330  symgextfv  16422  symgextfo  16426  symgfixfo  16443  pmtrprfval  16491  pmtrprfvalrn  16492  psgneu  16510  psgnval  16511  psgnvali  16512  psgnvalii  16513  odval  16537  dfod2  16565  submod  16568  isslw  16607  sylow2alem1  16616  sylow3lem2  16627  lsmelvalm  16650  lsmdisj2  16679  efgrelexlemb  16747  frgpup3lem  16774  cyggeninv  16865  cygabl  16872  gsumval3eu  16886  gsumval3OLD  16887  gsumval3lem2  16889  gsummpt1n0  16971  nn0gsumfz  16991  dprddisj2  17066  dprddisj2OLD  17067  dpjrid  17090  pgpfac1lem3  17107  f1rhm0to0ALT  17369  abveq0  17454  abvtrivd  17468  lss1d  17588  lspsn  17627  lspsnel  17628  lspprel  17719  rrgeq0i  17916  domneq0  17925  psrlidm  18035  psrlidmOLD  18036  psrridm  18037  psrridmOLD  18038  mvrval2  18057  mvrf1  18060  mplmonmul  18105  evlslem3  18162  coe1tm  18293  coe1tmfv2  18295  cply1coe0  18320  cply1coe0bi  18321  gsummoncoe1  18325  prmirredlem  18501  prmirredlemOLD  18504  znf1o  18568  znfld  18577  znunit  18580  cygznlem3  18586  psgndif  18616  ipeq0  18651  obsip  18730  frlmphl  18790  uvcvval  18795  ellspd  18814  ellspdOLD  18815  mamufacex  18869  mat1comp  18920  mat1dimelbas  18951  mat1dimid  18954  scmatel  18985  scmateALT  18992  mavmulsolcl  19031  marrepeval  19043  marepveval  19048  mdetunilem8  19099  maducoeval2  19120  madugsum  19123  minmar1eval  19129  symgmatr01lem  19133  symgmatr01  19134  gsummatr01lem3  19137  gsummatr01lem4  19138  gsummatr01  19139  m2cpm  19220  m2cpminvid2lem  19233  decpmatid  19249  monmatcollpw  19258  pmatcollpw3fi1lem1  19265  mp2pm2mplem4  19288  fvmptnn04ifc  19331  chfacffsupp  19335  chfacfscmul0  19337  chfacfscmulgsum  19339  chfacfpmmul0  19341  chfacfpmmulgsum  19343  cpmadumatpoly  19362  cayleyhamilton  19369  cayleyhamiltonALT  19370  eltopspOLD  19397  istpsOLD  19399  istopon  19404  fctop  19483  cctop  19485  ppttop  19486  pptbas  19487  epttop  19488  t0sep  19803  t1sep2  19848  cmpsublem  19877  cmpsub  19878  unisngl  20006  txuni2  20044  elpt  20051  ptbasfi  20060  xkoopn  20068  ptpjopn  20091  ptclsg  20094  dfac14lem  20096  ptcnp  20101  ptrescn  20118  tx1stc  20129  qtopeu  20195  kqt0lem  20215  isr0  20216  hauspwpwf1  20466  xmeteq0  20819  imasf1oxmet  20856  comet  20994  stdbdxmet  20996  met2ndci  21003  prdsxmslem2  21010  nrmmetd  21073  tngngp  21146  xrsxmet  21292  iccpnfcnv  21422  iccpnfhmeo  21423  cnheibor  21433  elovolm  21864  ovolgelb  21869  ovolicc1  21905  ovolicc  21912  ioorval  21961  uniioombllem6  21975  dyadmax  21985  dyadmbl  21987  i1fadd  22080  i1fmul  22081  itg1addlem3  22083  i1fmulc  22088  itg2l  22114  itg2leub  22119  limcmpt  22265  limcco  22275  dvcobr  22327  deg1ldg  22470  ig1pval  22551  elply  22570  elply2  22571  coeval  22598  coe1termlem  22633  coe1term  22634  quotval  22666  plydivlem4  22670  plydivex  22671  vieta1  22686  aannenlem2  22703  aalioulem2  22707  abelthlem9  22813  logtayllem  23018  logtayl  23019  isosctrlem2  23131  leibpilem2  23250  rlimcnp2  23274  efrlim  23277  dvdsmulf1o  23448  perfectlem2  23483  lgsfval  23554  lgsval2lem  23559  lgsdchrval  23600  2sqlem2  23617  2sqlem8  23625  2sqlem9  23626  2sqlem11  23628  dchrisum0flblem1  23671  padicval  23780  padicabv  23793  ostth1  23796  axtgcgrid  23838  axtgbtwnid  23841  islmib  24131  axpaschlem  24221  axlowdimlem15  24237  axlowdim  24242  cusgrafilem2  24458  cusgrafi  24460  wlkntrllem3  24541  fargshiftf1  24615  fargshiftfo  24616  constr3trllem2  24629  wwlkn0  24667  wlklniswwlkn1  24677  2wlkeq  24685  clwlkisclwwlklem2a1  24757  clwwlknscsh  24797  eleclclwwlkn  24811  hashecclwwlkn1  24812  usghashecclwwlk  24813  vdusgraval  24885  rusgranumwlkl1  24925  frgra3vlem1  24978  3vfriswmgralem  24982  frgrancvvdeqlem4  25011  2spotiundisj  25040  usgreghash2spotv  25044  frgregordn0  25048  numclwlk1lem2f1  25072  frgrareggt1  25094  gxval  25238  gxdi  25276  ismgmOLD  25300  nvz  25550  nmosetn0  25658  nmoolb  25664  nmoubi  25665  nmlno0lem  25686  nmlno0i  25687  hvsubeq0  25963  hvaddcan  25965  normsub0  26031  norm1exi  26146  pjhval  26293  omlsii  26299  omlsi  26300  pjoml  26332  h1de2ci  26452  spansneleq  26466  h1datomi  26477  h1datom  26478  spansncv  26549  5oalem6  26555  pj11  26610  nmopsetn0  26762  nmfnsetn0  26775  nmoplb  26804  nmopub  26805  nmfnlb  26821  nmfnleub  26822  nmlnop0iALT  26892  nmlnop0  26895  lnopeq  26906  nmopun  26911  nmcexi  26923  branmfn  27002  pjnmopi  27045  pj3i  27105  atss  27243  atom1d  27250  chirred  27292  cdj3lem2  27332  elabreximd  27386  disjxpin  27425  disjunsn  27431  br8d  27441  fmptcof2  27480  sgnsval  27696  xrge0iifcnv  27893  xrge0iifcv  27894  xrge0iifhom  27897  xrge0tmdOLD  27905  xrge0tmd  27906  esumc  28040  sgn3da  28458  sgnmul  28459  sgnnbi  28462  sgnpbi  28463  sgn0bi  28464  plymulx0  28482  signspval  28487  sconpi1  28662  cvmlift3lem2  28743  ghomf1olem  29012  relexp0  29030  relexpsucr  29031  relexpsucl  29033  rtrclreclem.trans  29047  br8  29161  br6  29162  br4  29163  rdgprc0  29202  dfrdg2  29204  sltval2  29392  sltintdifex  29399  sltres  29400  dfbigcup2  29525  elsingles  29544  dfiota3  29549  brimageg  29553  brdomaing  29561  brrangeg  29562  dfrdg4  29576  tfrqfree  29577  elaltxp  29601  funtransport  29657  fvtransport  29658  brsegle  29734  funray  29766  fvray  29767  funline  29768  fvline  29770  ellines  29778  linethru  29779  rankeq1o  29804  fin2so  30016  supaddc  30017  supadd  30018  ptrest  30024  heicant  30025  mblfinlem2  30028  mblfinlem3  30029  mblfinlem4  30030  ismblfin  30031  itg2addnclem  30042  itg2addnclem3  30044  itg2addnc  30045  ftc1anc  30074  subtr  30108  subtr2  30109  nn0prpw  30117  unirep  30179  f1opr  30191  sdclem2  30211  sdclem1  30212  sdc  30213  fdc  30214  isbnd  30252  heibor1lem  30281  heiborlem4  30286  heiborlem6  30288  heiborlem10  30292  maxidlmax  30416  prnc  30440  isfldidl  30441  dmnnzd  30448  elrfi  30602  nacsfg  30613  mzpcompact2lem  30660  eldioph2b  30672  eldioph3  30675  eldiophss  30684  diophrex  30685  elnn0rabdioph  30712  rencldnfilem  30730  elpell1qr  30759  elpell14qr  30761  elpell1234qr  30763  divalgmodcl  30905  jm2.27  30926  rmydioph  30932  expdiophlem2  30940  wepwsolem  30963  aomclem6  30981  lnr2i  31041  lpirlnr  31042  hbtlem2  31049  hbtlem4  31051  hbtlem5  31053  rngunsnply  31098  flcidc  31099  lcmval  31174  pm13.192  31271  refsum2cnlem1  31366  elabrexg  31384  upbdrech  31459  ssfiunibd  31463  iccshift  31512  iooshift  31516  limcperiod  31588  cncfshiftioo  31649  itgiccshift  31733  itgperiod  31734  stoweidlem46  31782  fourierdlem29  31872  fourierdlem37  31880  fourierdlem48  31891  fourierdlem51  31894  fourierdlem54  31897  fourierdlem62  31905  fourierdlem79  31922  fourierdlem81  31924  fourierdlem82  31925  fourierdlem92  31935  fourierdlem96  31939  fourierdlem97  31940  fourierdlem98  31941  fourierdlem99  31942  fourierdlem103  31946  fourierdlem104  31947  fourierdlem105  31948  fourierdlem108  31951  fourierdlem110  31953  fourierdlem112  31955  etransclem1  31972  etransclem5  31976  etransclem17  31988  etransclem32  32003  etransclem41  32012  afv0fv0  32188  afvfv0bi  32191  afvelrnb  32202  afvelrnb0  32203  otiunsndisjX  32255  2ffzoeq  32295  usgedgnlp  32364  usgedgvadf1  32369  usgedgvadf1ALT  32372  0nodd  32451  1odd  32452  2nodd  32453  tpres  32506  0even  32564  1neven  32565  2even  32566  2zlidl  32567  2zrngamgm  32572  2zrngagrp  32576  2zrngmmgm  32579  2zrngnmrid  32583  suppmptcfin  32842  lcoval  32883  linc0scn0  32894  linc1  32896  el0ldep  32937  snlindsntor  32942  equncomVD  33536  csbingVD  33552  csbsngVD  33561  csbfv12gALTVD  33567  relopabVD  33569  bnj1468  33772  riotasvd  34562  lshpdisj  34587  lsat0cv  34633  lcvexchlem4  34637  lcvexchlem5  34638  lshpkrlem1  34710  lshpkrlem2  34711  lshpkrlem3  34712  lshpkrcl  34716  islshpkrN  34720  atnle  34917  glbconxN  34977  isline  35338  ispointN  35341  pmapglbx  35368  ispsubcl2N  35546  lhp2atnle  35632  cdleme43fsv1snlem  36021  cdleme40v  36070  cdlemkid5  36536  cdlemkid  36537  dvhb1dimN  36587  dib1dim  36767  dicopelval  36779  dicelval1sta  36789  diclspsn  36796  dihvalcqpre  36837  dihglblem2aN  36895  dihglblem2N  36896  dih1dimatlem  36931  dihpN  36938  dochfl1  37078  lcfl7N  37103  lcf1o  37153  hvmapvalvalN  37363  hdmapval2lem  37436  frege55lem1c  37747
  Copyright terms: Public domain W3C validator