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

Theorem eqeq1 2433
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 23 . 2  |-  ( A  =  B  ->  A  =  B )
21eqeq1d 2431 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  eqeq1i  2436  eqeq2OLD  2445  eqeq12  2448  eqtr  2455  eqsb3lem  2548  clelab  2573  clelabOLD  2574  neeq1OLD  2713  pm13.18  2742  issetf  3092  sbhypf  3134  vtoclgft  3135  rexraleqim  3203  eqvincf  3205  pm13.183  3218  eueq  3249  mob  3259  euind  3264  reu2eqd  3274  reuind  3281  eqsbc3  3345  csbhypf  3420  uniiunlem  3555  snjust  4001  elprg  4018  elsncg  4025  rabrsn  4073  sneqrg  4172  preq12bg  4182  prel12g  4183  intab  4289  uniintsn  4296  dfiin2g  4335  disji2  4413  disjprg  4422  eusv1  4619  reusv2lem2  4627  reusv3  4633  opthg  4697  copsexg  4707  euotd  4722  otiunsndisj  4727  elopab  4729  solin  4798  elxpi  4870  opbrop  4934  relop  5005  ideqg  5006  elrnmpt  5101  elrnmpt1  5103  elrnmptg  5104  somin1  5253  cnveqb  5311  relcoi1OLD  5385  funopg  5633  f0rn0  5785  fvelrnb  5928  fvmptg  5962  fndmin  6004  eldmrexrn  6043  foelrn  6056  foco2  6057  fmptco  6071  fmptsng  6100  fmptsnd  6101  tpres  6132  eufnfv  6154  elabrex  6163  abrexco  6164  f1veqaeq  6176  isosolem  6253  f1oiso  6257  eusvobj2  6298  oprabid  6332  oprabv  6353  mpt2fun  6412  elrnmpt2g  6422  elrnmpt2  6423  elrnmpt2res  6424  ralrnmpt2  6425  ov3  6447  ov6g  6448  ovelrn  6459  caovcang  6484  caovcan  6487  snnex  6611  uniuni  6614  orduninsuc  6684  funcnvuni  6760  fun11iun  6767  f1oweALT  6791  opiota  6866  eloprabi  6869  frxp  6917  funsssuppss  6952  dftpos4  7000  tz7.44-2  7133  tz7.44-3  7134  oev  7224  oalimcl  7269  omlimcl  7287  odi  7288  omeu  7294  oeeui  7311  nneob  7361  omopth  7367  elqsg  7423  qsdisj  7448  qsel  7450  brecop  7464  eroveu  7466  erovlem  7467  elixpsn  7569  ixpsnf1o  7570  boxcutc  7573  2dom  7649  fundmen  7650  xpf1o  7740  nneneq  7761  fofinf1o  7858  elfi  7933  elfiun  7950  dffi3  7951  brwdom  8082  brwdom3  8097  unwdomg  8099  xpwdomg  8100  noinfep  8164  cantnfp1lem1  8182  cantnfp1lem3  8184  cantnflem1  8193  scott0  8356  carden2a  8399  cardiun  8415  pm54.43lem  8432  alephval3  8539  dfac5lem3  8554  dfac5lem4  8555  dfac2  8559  kmlem9  8586  kmlem12  8589  cardcf  8680  cfeq0  8684  cfsuc  8685  cff1  8686  cflim2  8691  cfss  8693  isfin5  8727  fin1a2lem11  8838  fin1a2lem13  8840  brdom7disj  8957  brdom6disj  8958  canthp1lem2  9077  canthp1  9078  tskuni  9207  gruina  9242  genpv  9423  genpelv  9424  addsrmo  9496  mulsrmo  9497  ltsosr  9517  ltresr  9563  axcnre  9587  axpre-lttri  9588  ltordlem  10138  ltord1  10139  fimaxre3  10553  supaddc  10574  supadd  10575  supmul1  10576  supmullem1  10577  supmullem2  10578  supmul  10579  creur  10603  creui  10604  nn1m1nn  10629  elz  10939  nn0ind-raph  11035  xnegeq  11500  xmullem2  11551  xmulasslem  11571  fleqceilz  12078  fseqsupubi  12188  sqeqor  12385  nn0opth2  12455  hash1snb  12588  hash2prde  12625  hash2prd  12627  hash2pwpr  12628  brfi1uzind  12641  wrd2ind  12819  cshfn  12877  2cshwcshw  12909  scshwfzeqfzo  12910  relexpsucnnr  13067  relexprelg  13080  rtrclreclem3  13102  shftfval  13112  sgnval  13130  sqrlem6  13290  summo  13761  fsum  13764  telfsumo  13840  infcvgaux1i  13893  infcvgaux2i  13894  mertenslem1  13918  mertenslem2  13919  mertens  13920  prodmo  13968  fprod  13973  ruclem12  14271  divalg  14359  ndvdssub  14363  sadcp1  14403  smupp1  14428  gcdval  14444  bezoutlem1  14477  bezoutlem3  14479  bezoutlem4  14480  bezout  14481  lcmval  14522  dvdsprime  14599  nprm  14600  dvdsprm  14609  coprmgcdb  14616  coprm  14619  qnumval  14648  qdenval  14649  m1dvdsndvds  14703  reumodprminv  14709  pcval  14748  pceu  14750  pczpre  14751  pcdiv  14756  4sqlem2  14847  4sqlem4  14850  4sqlem12  14854  4sq  14868  vdwapval  14877  vdwapun  14878  vdwlem6  14890  cshwrepswhash1  15027  acsfn  15507  initoid  15842  termoid  15843  posi  16137  gsumval2a  16464  mgm2nsgrplem2  16595  mgm2nsgrplem3  16596  sgrp2nmndlem5  16605  mgmnsgrpex  16607  sgrpnmndex  16608  ghmf1  16853  conjnmzb  16859  orbsta  16909  symgextfv  17001  symgextfo  17005  symgfixfo  17022  pmtrprfval  17070  pmtrprfvalrn  17071  psgneu  17089  psgnval  17090  psgnvali  17091  psgnvalii  17092  odval  17116  dfod2  17144  submod  17147  isslw  17186  sylow2alem1  17195  sylow3lem2  17206  lsmelvalm  17229  lsmdisj2  17258  efgrelexlemb  17326  frgpup3lem  17353  cyggeninv  17444  cygabl  17451  gsumval3eu  17464  gsumval3lem2  17466  gsummpt1n0  17523  nn0gsumfz  17539  dprddisj2  17598  dpjrid  17621  pgpfac1lem3  17636  f1rhm0to0ALT  17895  abveq0  17980  abvtrivd  17994  lss1d  18112  lspsn  18151  lspsnel  18152  lspprel  18243  rrgeq0i  18439  domneq0  18447  psrlidm  18553  psrridm  18554  mvrval2  18572  mvrf1  18575  mplmonmul  18614  evlslem3  18663  coe1tm  18792  coe1tmfv2  18794  cply1coe0  18819  cply1coe0bi  18820  gsummoncoe1  18824  prmirredlem  18986  znf1o  19044  znfld  19053  znunit  19056  cygznlem3  19062  psgndif  19092  ipeq0  19127  obsip  19206  frlmphl  19261  uvcvval  19266  ellspd  19282  mamufacex  19336  mat1comp  19387  mat1dimelbas  19418  mat1dimid  19421  scmatel  19452  scmateALT  19459  mavmulsolcl  19498  marrepeval  19510  marepveval  19515  mdetunilem8  19566  maducoeval2  19587  madugsum  19590  minmar1eval  19596  symgmatr01lem  19600  symgmatr01  19601  gsummatr01lem3  19604  gsummatr01lem4  19605  gsummatr01  19606  m2cpm  19687  m2cpminvid2lem  19700  decpmatid  19716  monmatcollpw  19725  pmatcollpw3fi1lem1  19732  mp2pm2mplem4  19755  fvmptnn04ifc  19798  chfacffsupp  19802  chfacfscmul0  19804  chfacfscmulgsum  19806  chfacfpmmul0  19808  chfacfpmmulgsum  19810  cpmadumatpoly  19829  cayleyhamilton  19836  cayleyhamiltonALT  19837  istopon  19862  fctop  19941  cctop  19943  ppttop  19944  pptbas  19945  epttop  19946  t0sep  20262  t1sep2  20307  cmpsublem  20336  cmpsub  20337  unisngl  20464  txuni2  20502  elpt  20509  ptbasfi  20518  xkoopn  20526  ptpjopn  20549  ptclsg  20552  dfac14lem  20554  ptcnp  20559  ptrescn  20576  tx1stc  20587  qtopeu  20653  kqt0lem  20673  isr0  20674  hauspwpwf1  20924  xmeteq0  21275  imasf1oxmet  21312  comet  21450  stdbdxmet  21452  met2ndci  21459  prdsxmslem2  21466  nrmmetd  21511  tngngp  21584  xrsxmet  21729  iccpnfcnv  21859  iccpnfhmeo  21860  cnheibor  21870  elovolm  22297  ovolgelb  22302  ovolicc1  22338  ovolicc  22345  ioorval  22394  ioorvalOLD  22399  uniioombllem6  22414  dyadmax  22424  dyadmbl  22426  i1fadd  22521  i1fmul  22522  itg1addlem3  22524  i1fmulc  22529  itg2l  22555  itg2leub  22560  limcmpt  22706  limcco  22716  dvcobr  22768  deg1ldg  22909  ig1pval  22989  elply  23008  elply2  23009  coeval  23036  coe1termlem  23071  coe1term  23072  quotval  23104  plydivlem4  23108  plydivex  23109  vieta1  23124  aannenlem2  23141  aalioulem2  23145  abelthlem9  23251  logtayllem  23460  logtayl  23461  isosctrlem2  23604  leibpilem2  23723  rlimcnp2  23748  efrlim  23751  dvdsmulf1o  23977  perfectlem2  24012  lgsfval  24083  lgsval2lem  24088  lgsdchrval  24129  2sqlem2  24146  2sqlem8  24154  2sqlem9  24155  2sqlem11  24157  dchrisum0flblem1  24200  padicval  24309  padicabv  24322  ostth1  24325  axtgcgrid  24365  axtgbtwnid  24368  islmib  24676  axpaschlem  24807  axlowdimlem15  24823  axlowdim  24828  cusgrafilem2  25044  cusgrafi  25046  wlkntrllem3  25127  fargshiftf1  25201  fargshiftfo  25202  constr3trllem2  25215  wwlkn0  25253  wlklniswwlkn1  25263  2wlkeq  25271  clwlkisclwwlklem2a1  25343  clwwlknscsh  25383  eleclclwwlkn  25397  hashecclwwlkn1  25398  usghashecclwwlk  25399  vdusgraval  25471  rusgranumwlkl1  25511  frgra3vlem1  25564  3vfriswmgralem  25568  frgrancvvdeqlem4  25597  2spotiundisj  25626  usgreghash2spotv  25630  frgregordn0  25634  numclwlk1lem2f1  25658  frgrareggt1  25680  gxval  25822  gxdi  25860  ismgmOLD  25884  nvz  26134  nmosetn0  26242  nmoolb  26248  nmoubi  26249  nmlno0lem  26270  nmlno0i  26271  hvsubeq0  26547  hvaddcan  26549  normsub0  26615  norm1exi  26729  pjhval  26876  omlsii  26882  omlsi  26883  pjoml  26915  h1de2ci  27035  spansneleq  27049  h1datomi  27060  h1datom  27061  spansncv  27132  5oalem6  27138  pj11  27193  nmopsetn0  27344  nmfnsetn0  27357  nmoplb  27386  nmopub  27387  nmfnlb  27403  nmfnleub  27404  nmlnop0iALT  27474  nmlnop0  27477  lnopeq  27488  nmopun  27493  nmcexi  27505  branmfn  27584  pjnmopi  27627  pj3i  27687  atss  27825  atom1d  27832  chirred  27874  cdj3lem2  27914  elabreximd  27971  disjxpin  28028  disjunsn  28034  br8d  28048  fmptcof2  28090  sgnsval  28320  psgnfzto1stlem  28443  madjusmdetlem2  28484  madjusmdet  28487  xrge0iifcnv  28569  xrge0iifcv  28570  xrge0iifhom  28573  xrge0tmdOLD  28581  xrge0tmd  28582  esumc  28702  sgn3da  29191  sgnmul  29192  sgnnbi  29195  sgnpbi  29196  sgn0bi  29197  plymulx0  29215  signspval  29220  bnj1468  29436  sconpi1  29741  cvmlift3lem2  29822  ghomf1olem  30091  br8  30174  br6  30175  br4  30176  br1steqg  30194  br2ndeqg  30195  rdgprc0  30218  dfrdg2  30220  sltval2  30321  sltintdifex  30328  sltres  30329  dfbigcup2  30442  elsingles  30461  dfiota3  30466  brimageg  30470  brdomaing  30478  brrangeg  30479  dfrdg4  30494  elaltxp  30518  funtransport  30574  fvtransport  30575  brsegle  30651  funray  30683  fvray  30684  funline  30685  fvline  30687  ellines  30695  linethru  30696  rankeq1o  30714  subtr  30746  subtr2  30747  nn0prpw  30755  topdifinffinlem  31475  topdifinffin  31476  topdifinfeq  31478  fin2so  31626  ptrest  31633  poimirlem25  31659  poimirlem26  31660  poimirlem27  31661  poimirlem28  31662  poimirlem31  31665  poimirlem32  31666  heicant  31669  mblfinlem2  31672  mblfinlem3  31673  mblfinlem4  31674  ismblfin  31675  itg2addnclem  31687  itg2addnclem3  31689  itg2addnc  31690  ftc1anc  31719  unirep  31733  f1opr  31745  sdclem2  31765  sdclem1  31766  sdc  31767  fdc  31768  isbnd  31806  heibor1lem  31835  heiborlem4  31840  heiborlem6  31842  heiborlem10  31846  maxidlmax  31970  prnc  31994  isfldidl  31995  dmnnzd  32002  riotasvd  32227  lshpdisj  32252  lsat0cv  32298  lcvexchlem4  32302  lcvexchlem5  32303  lshpkrlem1  32375  lshpkrlem2  32376  lshpkrlem3  32377  lshpkrcl  32381  islshpkrN  32385  atnle  32582  glbconxN  32642  isline  33003  ispointN  33006  pmapglbx  33033  ispsubcl2N  33211  lhp2atnle  33297  cdleme43fsv1snlem  33686  cdleme40v  33735  cdlemkid5  34201  cdlemkid  34202  dvhb1dimN  34252  dib1dim  34432  dicopelval  34444  dicelval1sta  34454  diclspsn  34461  dihvalcqpre  34502  dihglblem2aN  34560  dihglblem2N  34561  dih1dimatlem  34596  dihpN  34603  dochfl1  34743  lcfl7N  34768  lcf1o  34818  hvmapvalvalN  35028  hdmapval2lem  35101  elrfi  35235  nacsfg  35246  mzpcompact2lem  35292  eldioph2b  35304  eldioph3  35307  eldiophss  35316  diophrex  35317  elnn0rabdioph  35345  rencldnfilem  35362  elpell1qr  35391  elpell14qr  35393  elpell1234qr  35395  divalgmodcl  35538  jm2.27  35559  rmydioph  35565  expdiophlem2  35573  wepwsolem  35596  aomclem6  35613  lnr2i  35671  lpirlnr  35672  hbtlem2  35679  hbtlem4  35681  hbtlem5  35683  rngunsnply  35728  flcidc  35729  brtrclfv2  35948  frege55lem1c  36139  frege104  36190  pm13.192  36388  equncomVD  36895  csbingVD  36911  csbsngVD  36920  csbfv12gALTVD  36926  relopabVD  36928  refsum2cnlem1  36988  elabrexg  37000  elrnmptf  37067  foelrnf  37074  disjinfi  37081  upbdrech  37122  ssfiunibd  37126  iccshift  37194  iooshift  37198  fsumf1of  37218  limcperiod  37270  cncfshiftioo  37332  itgiccshift  37416  itgperiod  37417  stoweidlem46  37466  fourierdlem29  37557  fourierdlem37  37565  fourierdlem48  37576  fourierdlem51  37579  fourierdlem54  37582  fourierdlem62  37590  fourierdlem79  37607  fourierdlem81  37609  fourierdlem82  37610  fourierdlem92  37620  fourierdlem96  37624  fourierdlem97  37625  fourierdlem98  37626  fourierdlem99  37627  fourierdlem103  37631  fourierdlem104  37632  fourierdlem105  37633  fourierdlem108  37636  fourierdlem110  37638  fourierdlem112  37640  etransclem1  37657  etransclem5  37661  etransclem17  37673  etransclem32  37688  etransclem41  37697  sge0f1o  37748  sge0resplit  37772  sge0fodjrnlem  37782  nnfoctbdjlem  37792  nnfoctbdj  37793  afv0fv0  38031  afvfv0bi  38034  afvelrnb  38045  afvelrnb0  38046  mod2eq1n2dvds  38105  m1expevenALTV  38157  odd2np1ALTV  38183  opoeALTV  38192  opeoALTV  38193  perfectALTVlem2  38224  isgbe  38232  isgbo  38233  isgboa  38234  sgoldbalt  38262  nnsum3primesgbe  38267  nnsum3primesle9  38269  nnsum4primesodd  38271  nnsum4primesoddALTV  38272  pfx2  38333  otiunsndisjX  38368  2ffzoeq  38403  usgedgnlp  38470  usgedgvadf1  38475  usgedgvadf1ALT  38478  0nodd  38558  1odd  38559  2nodd  38560  0even  38679  1neven  38680  2even  38681  2zlidl  38682  2zrngamgm  38687  2zrngagrp  38691  2zrngmmgm  38694  2zrngnmrid  38698  suppmptcfin  38914  lcoval  38955  linc0scn0  38966  linc1  38968  el0ldep  39009  snlindsntor  39014  blenval  39133  nn0sumshdiglemB  39182
  Copyright terms: Public domain W3C validator