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

Theorem eqeq1 2471
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 2469 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  eqeq1i  2474  eqeq2OLD  2483  eqeq12  2486  eqtr  2493  eqsb3lem  2586  clelab  2611  clelabOLD  2612  neeq1OLD  2749  pm13.18  2778  issetf  3118  sbhypf  3160  vtoclgft  3161  rexraleqim  3229  eqvincf  3231  pm13.183  3244  eueq  3275  mob  3285  euind  3290  reu2eqd  3300  reuind  3307  eqsbc3  3371  csbhypf  3454  uniiunlem  3588  snjust  4026  elprg  4043  elsncg  4050  rabrsn  4097  sneqrg  4196  preq12bg  4205  prel12g  4206  intab  4312  uniintsn  4319  dfiin2g  4358  disji2  4434  disjprg  4443  eusv1  4641  reusv2lem2  4649  reusv3  4655  reusv6OLD  4658  opthg  4722  copsexg  4732  copsexgOLD  4733  euotd  4748  otiunsndisj  4753  elopab  4755  solin  4823  elxpi  5015  opbrop  5077  relop  5151  ideqg  5152  elrnmpt  5247  elrnmpt1  5249  elrnmptg  5250  somin1  5401  cnveqb  5460  relcoi1  5534  funopg  5618  f0rn0  5768  fvelrnb  5913  fvmptg  5946  fndmin  5986  eldmrexrn  6025  foelrn  6038  foco2  6039  fmptco  6052  fmptsng  6080  fmptsnd  6081  eufnfv  6132  elabrex  6141  abrexco  6142  f1veqaeq  6154  isosolem  6229  f1oiso  6233  eusvobj2  6275  oprabid  6306  oprabv  6327  mpt2fun  6386  elrnmpt2g  6396  elrnmpt2  6397  elrnmpt2res  6398  ralrnmpt2  6399  ov3  6421  ov6g  6422  ovelrn  6433  caovcang  6458  caovcan  6461  snnex  6584  uniuni  6587  orduninsuc  6656  funcnvuni  6734  fun11iun  6741  f1oweALT  6765  opiota  6840  eloprabi  6843  frxp  6890  funsssuppss  6923  dftpos4  6971  tz7.44-2  7070  tz7.44-3  7071  oev  7161  oalimcl  7206  omlimcl  7224  odi  7225  omeu  7231  oeeui  7248  nneob  7298  omopth  7304  elqsg  7360  qsdisj  7385  qsel  7387  brecop  7401  eroveu  7403  erovlem  7404  elixpsn  7505  ixpsnf1o  7506  boxcutc  7509  2dom  7585  fundmen  7586  xpf1o  7676  nneneq  7697  fofinf1o  7797  elfi  7869  elfiun  7886  dffi3  7887  brwdom  7989  brwdom3  8004  unwdomg  8006  xpwdomg  8007  noinfep  8072  cantnfp1lem1  8093  cantnfp1lem3  8095  cantnflem1  8104  cantnfp1lem1OLD  8119  cantnfp1lem3OLD  8121  cantnfp1OLD  8122  cantnflem1OLD  8127  scott0  8300  carden2a  8343  cardiun  8359  pm54.43lem  8376  alephval3  8487  dfac5lem3  8502  dfac5lem4  8503  dfac2  8507  kmlem9  8534  kmlem12  8537  cardcf  8628  cfeq0  8632  cfsuc  8633  cff1  8634  cflim2  8639  cfss  8641  isfin5  8675  fin1a2lem11  8786  fin1a2lem13  8788  brdom7disj  8905  brdom6disj  8906  canthp1lem2  9027  canthp1  9028  tskuni  9157  gruina  9192  genpv  9373  genpelv  9374  addsrmo  9446  mulsrmo  9447  ltsosr  9467  ltresr  9513  axcnre  9537  axpre-lttri  9538  ltordlem  10074  ltord1  10075  fimaxre3  10488  supmul1  10504  supmullem1  10505  supmullem2  10506  supmul  10507  creur  10526  creui  10527  nn1m1nn  10552  elz  10862  nn0ind-raph  10957  xnegeq  11402  xmullem2  11453  xmulasslem  11473  fleqceilz  11944  fseqsupubi  12051  sqeqor  12244  nn0opth2  12314  hash1snb  12438  euhash1  12439  hash2prde  12476  hash2prd  12478  hash2pwpr  12479  brfi1uzind  12492  wrd2ind  12660  cshfn  12718  2cshwcshw  12750  scshwfzeqfzo  12751  ccatco  12758  shftfval  12860  sgnval  12878  sqrlem6  13038  summo  13495  fsum  13498  telfsumo  13572  infcvgaux1i  13624  infcvgaux2i  13625  mertenslem1  13649  mertenslem2  13650  mertens  13651  ruclem12  13828  divalg  13913  ndvdssub  13917  bitsinvp1  13951  sadcp1  13957  smupp1  13982  gcdval  13998  bezoutlem1  14028  bezoutlem3  14030  bezoutlem4  14031  bezout  14032  dvdsprime  14082  nprm  14083  dvdsprm  14092  coprm  14093  qnumval  14122  qdenval  14123  m1dvdsndvds  14177  reumodprminv  14181  pcval  14220  pceu  14222  pczpre  14223  pcdiv  14228  4sqlem2  14319  4sqlem4  14322  4sqlem12  14326  4sq  14334  vdwapval  14343  vdwapun  14344  vdwlem6  14356  cshwrepswhash1  14438  acsfn  14907  posi  15430  gsumval2a  15822  ghmf1  16087  conjnmzb  16093  orbsta  16143  symgextfv  16235  symgextfo  16239  symgfixfo  16257  pmtrprfval  16305  pmtrprfvalrn  16306  psgneu  16324  psgnval  16325  psgnvali  16326  psgnvalii  16327  odval  16351  dfod2  16379  submod  16382  isslw  16421  sylow2alem1  16430  sylow3lem2  16441  lsmelvalm  16464  lsmdisj2  16493  efgrelexlemb  16561  frgpup3lem  16588  cyggeninv  16674  cygabl  16681  gsumval3eu  16695  gsumval3OLD  16696  gsumval3lem2  16698  gsummpt1n0  16780  nn0gsumfz  16800  dprddisj2  16874  dprddisj2OLD  16875  dpjrid  16898  pgpfac1lem3  16915  f1rhm0to0ALT  17170  abveq0  17255  abvtrivd  17269  lss1d  17389  lspsn  17428  lspsnel  17429  lspprel  17520  rrgeq0i  17705  domneq0  17714  psrlidm  17824  psrlidmOLD  17825  psrridm  17826  psrridmOLD  17827  mvrval2  17846  mvrf1  17849  mplmonmul  17894  evlslem3  17951  coe1tm  18082  coe1tmfv2  18084  cply1coe0  18109  cply1coe0bi  18110  gsummoncoe1  18114  xrsdsreval  18228  prmirredlem  18287  prmirredlemOLD  18290  znf1o  18354  znfld  18363  znunit  18366  cygznlem3  18372  psgndif  18402  ipeq0  18437  obsip  18516  frlmphl  18576  uvcvval  18581  ellspd  18600  ellspdOLD  18601  mamufacex  18655  mat1comp  18706  mat1dimelbas  18737  mat1dimid  18740  scmatel  18771  scmateALT  18778  mavmulsolcl  18817  marrepeval  18829  marepveval  18834  mdetunilem8  18885  maducoeval2  18906  madugsum  18909  minmar1eval  18915  symgmatr01lem  18919  symgmatr01  18920  gsummatr01lem3  18923  gsummatr01lem4  18924  gsummatr01  18925  m2cpm  19006  m2cpminvid2lem  19019  decpmatid  19035  monmatcollpw  19044  pmatcollpw3fi1lem1  19051  mp2pm2mplem4  19074  fvmptnn04ifc  19117  chfacffsupp  19121  chfacfscmul0  19123  chfacfscmulgsum  19125  chfacfpmmul0  19127  chfacfpmmulgsum  19129  cpmadumatpoly  19148  cayleyhamilton  19155  cayleyhamiltonALT  19156  eltopspOLD  19183  istpsOLD  19185  istopon  19190  fctop  19268  cctop  19270  ppttop  19271  pptbas  19272  epttop  19273  t0sep  19588  t1sep2  19633  cmpsublem  19662  cmpsub  19663  txuni2  19798  elpt  19805  ptbasfi  19814  xkoopn  19822  ptpjopn  19845  ptclsg  19848  dfac14lem  19850  ptcnp  19855  ptrescn  19872  tx1stc  19883  qtopeu  19949  kqt0lem  19969  isr0  19970  hauspwpwf1  20220  xmeteq0  20573  imasf1oxmet  20610  comet  20748  stdbdxmet  20750  met2ndci  20757  prdsxmslem2  20764  nrmmetd  20827  tngngp  20900  xrsxmet  21046  iccpnfcnv  21176  iccpnfhmeo  21177  oprpiece1res2  21184  cnheibor  21187  phtpycc  21223  elovolm  21618  ovolgelb  21623  ovolicc1  21659  ovolicc  21666  ioorval  21715  uniioombllem6  21729  dyadmax  21739  dyadmbl  21741  i1fadd  21834  i1fmul  21835  itg1addlem3  21837  i1fmulc  21842  itg2l  21868  itg2leub  21873  limcmpt  22019  limcco  22029  dvcobr  22081  deg1ldg  22224  ig1pval  22305  elply  22324  elply2  22325  coeval  22352  coe1termlem  22386  coe1term  22387  quotval  22419  plydivlem4  22423  plydivex  22424  vieta1  22439  aannenlem2  22456  aalioulem2  22460  abelthlem9  22566  logtayllem  22765  logtayl  22766  isosctrlem2  22878  atantayl2  22994  leibpilem2  22997  rlimcnp2  23021  efrlim  23024  dvdsmulf1o  23195  perfectlem2  23230  lgsfval  23301  lgsval2lem  23306  lgsdchrval  23347  2sqlem2  23364  2sqlem8  23372  2sqlem9  23373  2sqlem11  23375  dchrisum0flblem1  23418  padicval  23527  padicabv  23540  ostth1  23543  axtgcgrid  23585  axtgbtwnid  23588  islmib  23827  axpaschlem  23916  axlowdimlem15  23932  axlowdim  23937  cusgrafilem2  24153  cusgrafi  24155  wlkntrllem3  24236  fargshiftf1  24310  fargshiftfo  24311  constr3trllem2  24324  wwlkn0  24362  wlklniswwlkn1  24372  2wlkeq  24380  clwlkisclwwlklem2a1  24452  clwwlknscsh  24492  eleclclwwlkn  24506  hashecclwwlkn1  24507  usghashecclwwlk  24508  vdusgraval  24580  rusgranumwlkl1  24620  frgra3vlem1  24673  3vfriswmgralem  24677  frgrancvvdeqlem4  24707  2spotiundisj  24736  usgreghash2spotv  24740  frgregordn0  24744  numclwlk1lem2f1  24768  frgrareggt1  24790  gxval  24933  gxdi  24971  ismgm  24995  nvz  25245  nmosetn0  25353  nmoolb  25359  nmoubi  25360  nmlno0lem  25381  nmlno0i  25382  hvsubeq0  25658  hvaddcan  25660  normsub0  25726  norm1exi  25841  pjhval  25988  omlsii  25994  omlsi  25995  pjoml  26027  h1de2ci  26147  spansneleq  26161  h1datomi  26172  h1datom  26173  spansncv  26244  5oalem6  26250  pj11  26305  nmopsetn0  26457  nmfnsetn0  26470  nmoplb  26499  nmopub  26500  nmfnlb  26516  nmfnleub  26517  nmlnop0iALT  26587  nmlnop0  26590  lnopeq  26601  nmopun  26606  nmcexi  26618  branmfn  26697  pjnmopi  26740  pj3i  26800  atss  26938  atom1d  26945  chirred  26987  cdj3lem2  27027  elabreximd  27079  disjxpin  27117  disjunsn  27123  br8d  27133  fmptcof2  27171  sgnsval  27377  xrge0iifcnv  27548  xrge0iifcv  27549  xrge0iifhom  27552  xrge0tmdOLD  27560  xrge0tmd  27561  esumc  27699  sgn3da  28117  sgnmul  28118  sgnnbi  28121  sgnpbi  28122  sgn0bi  28123  ccatmulgnn0dir  28133  plymulx0  28141  plymulx  28142  signspval  28146  sconpi1  28321  cvmlift3lem2  28402  ghomf1olem  28506  relexp0  28524  relexpsucr  28525  relexpsucl  28527  rtrclreclem.trans  28541  prodmo  28642  fprod  28647  br8  28759  br6  28760  br4  28761  rdgprc0  28800  dfrdg2  28802  sltval2  28990  sltintdifex  28997  sltres  28998  dfbigcup2  29123  elsingles  29142  dfiota3  29147  brimageg  29151  brdomaing  29159  brrangeg  29160  dfrdg4  29174  tfrqfree  29175  elaltxp  29199  funtransport  29255  fvtransport  29256  brsegle  29332  funray  29364  fvray  29365  funline  29366  fvline  29368  ellines  29376  linethru  29377  rankeq1o  29402  fin2so  29614  supaddc  29615  supadd  29616  ptrest  29623  heicant  29624  mblfinlem1  29626  mblfinlem2  29627  mblfinlem3  29628  mblfinlem4  29629  ismblfin  29630  itg2addnclem  29641  itg2addnclem3  29643  itg2addnc  29644  ftc1anc  29673  subtr  29707  subtr2  29708  nn0prpw  29716  unirep  29804  f1opr  29816  sdclem2  29836  sdclem1  29837  sdc  29838  fdc  29839  isbnd  29877  heibor1lem  29906  heiborlem4  29911  heiborlem6  29913  heiborlem10  29917  maxidlmax  30041  prnc  30065  isfldidl  30066  dmnnzd  30073  elrfi  30228  nacsfg  30239  mzpcompact2lem  30286  eldioph2b  30298  eldioph3  30301  eldiophss  30310  diophrex  30311  elnn0rabdioph  30338  rencldnfilem  30356  elpell1qr  30385  elpell14qr  30387  elpell1234qr  30389  divalgmodcl  30533  jm2.27  30554  rmydioph  30560  expdiophlem2  30568  wepwsolem  30591  aomclem6  30609  lnr2i  30669  lpirlnr  30670  hbtlem2  30677  hbtlem4  30679  hbtlem5  30681  rngunsnply  30727  flcidc  30728  lcmval  30798  pm13.192  30895  refsum2cnlem1  30990  elabrexg  31012  upbdrech  31082  ssfiunibd  31086  iccshift  31122  iooshift  31126  limcperiod  31170  cncfshiftioo  31231  itgiccshift  31298  itgperiod  31299  stoweidlem46  31346  fourierdlem29  31436  fourierdlem37  31444  fourierdlem48  31455  fourierdlem51  31458  fourierdlem54  31461  fourierdlem62  31469  fourierdlem79  31486  fourierdlem81  31488  fourierdlem82  31489  fourierdlem92  31499  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem103  31510  fourierdlem104  31511  fourierdlem105  31512  fourierdlem108  31515  fourierdlem110  31517  fourierdlem112  31519  afv0fv0  31701  afvfv0bi  31704  afvelrnb  31715  afvelrnb0  31716  otiunsndisjX  31768  2ffzoeq  31810  usgedgnlp  31879  usgedgvadf1  31884  usgedgvadf1ALT  31887  suppmptcfin  32045  lcoval  32086  linc0scn0  32097  linc1  32099  el0ldep  32140  snlindsntor  32145  equncomVD  32748  csbingVD  32764  csbsngVD  32773  csbfv12gALTVD  32779  relopabVD  32781  bnj1468  32983  riotasvd  33759  lshpdisj  33784  lsat0cv  33830  lcvexchlem4  33834  lcvexchlem5  33835  lshpkrlem1  33907  lshpkrlem2  33908  lshpkrlem3  33909  lshpkrcl  33913  islshpkrN  33917  atnle  34114  glbconxN  34174  isline  34535  ispointN  34538  pmapglbx  34565  ispsubcl2N  34743  lhp2atnle  34829  cdleme43fsv1snlem  35216  cdleme40v  35265  cdlemkid5  35731  cdlemkid  35732  dvhb1dimN  35782  dib1dim  35962  dicopelval  35974  dicelval1sta  35984  diclspsn  35991  dihvalcqpre  36032  dihglblem2aN  36090  dihglblem2N  36091  dih1dimatlem  36126  dihpN  36133  dochfl1  36273  lcfl7N  36298  lcf1o  36348  hvmapvalvalN  36558  hdmapval2lem  36631  frege55lem1c  36908
  Copyright terms: Public domain W3C validator