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

Theorem eqeq1 2386
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 2384 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-cleq 2374
This theorem is referenced by:  eqeq1i  2389  eqeq2OLD  2398  eqeq12  2401  eqtr  2408  eqsb3lem  2501  clelab  2526  clelabOLD  2527  neeq1OLD  2664  pm13.18  2693  issetf  3039  sbhypf  3081  vtoclgft  3082  rexraleqim  3150  eqvincf  3152  pm13.183  3165  eueq  3196  mob  3206  euind  3211  reu2eqd  3221  reuind  3228  eqsbc3  3292  csbhypf  3367  uniiunlem  3502  snjust  3943  elprg  3960  elsncg  3967  rabrsn  4014  sneqrg  4113  preq12bg  4123  prel12g  4124  intab  4230  uniintsn  4237  dfiin2g  4276  disji2  4354  disjprg  4363  eusv1  4559  reusv2lem2  4567  reusv3  4573  opthg  4637  copsexg  4647  euotd  4662  otiunsndisj  4667  elopab  4669  solin  4737  elxpi  4929  opbrop  4993  relop  5066  ideqg  5067  elrnmpt  5162  elrnmpt1  5164  elrnmptg  5165  somin1  5313  cnveqb  5371  relcoi1OLD  5445  funopg  5528  f0rn0  5678  fvelrnb  5821  fvmptg  5855  fndmin  5896  eldmrexrn  5939  foelrn  5952  foco2  5953  fmptco  5966  fmptsng  5994  fmptsnd  5995  tpres  6026  eufnfv  6047  elabrex  6056  abrexco  6057  f1veqaeq  6069  isosolem  6144  f1oiso  6148  eusvobj2  6189  oprabid  6223  oprabv  6244  mpt2fun  6303  elrnmpt2g  6313  elrnmpt2  6314  elrnmpt2res  6315  ralrnmpt2  6316  ov3  6338  ov6g  6339  ovelrn  6350  caovcang  6375  caovcan  6378  snnex  6505  uniuni  6508  orduninsuc  6577  funcnvuni  6652  fun11iun  6659  f1oweALT  6683  opiota  6758  eloprabi  6761  frxp  6809  funsssuppss  6844  dftpos4  6892  tz7.44-2  6991  tz7.44-3  6992  oev  7082  oalimcl  7127  omlimcl  7145  odi  7146  omeu  7152  oeeui  7169  nneob  7219  omopth  7225  elqsg  7281  qsdisj  7306  qsel  7308  brecop  7322  eroveu  7324  erovlem  7325  elixpsn  7427  ixpsnf1o  7428  boxcutc  7431  2dom  7507  fundmen  7508  xpf1o  7598  nneneq  7619  fofinf1o  7716  elfi  7788  elfiun  7805  dffi3  7806  brwdom  7908  brwdom3  7923  unwdomg  7925  xpwdomg  7926  noinfep  7990  cantnfp1lem1  8010  cantnfp1lem3  8012  cantnflem1  8021  cantnfp1lem1OLD  8036  cantnfp1lem3OLD  8038  cantnfp1OLD  8039  cantnflem1OLD  8044  scott0  8217  carden2a  8260  cardiun  8276  pm54.43lem  8293  alephval3  8404  dfac5lem3  8419  dfac5lem4  8420  dfac2  8424  kmlem9  8451  kmlem12  8454  cardcf  8545  cfeq0  8549  cfsuc  8550  cff1  8551  cflim2  8556  cfss  8558  isfin5  8592  fin1a2lem11  8703  fin1a2lem13  8705  brdom7disj  8822  brdom6disj  8823  canthp1lem2  8942  canthp1  8943  tskuni  9072  gruina  9107  genpv  9288  genpelv  9289  addsrmo  9361  mulsrmo  9362  ltsosr  9382  ltresr  9428  axcnre  9452  axpre-lttri  9453  ltordlem  9995  ltord1  9996  fimaxre3  10408  supmul1  10424  supmullem1  10425  supmullem2  10426  supmul  10427  creur  10446  creui  10447  nn1m1nn  10472  elz  10783  nn0ind-raph  10879  xnegeq  11327  xmullem2  11378  xmulasslem  11398  fleqceilz  11881  fseqsupubi  11991  sqeqor  12184  nn0opth2  12254  hash1snb  12383  hash2prde  12420  hash2prd  12422  hash2pwpr  12423  brfi1uzind  12436  wrd2ind  12614  cshfn  12672  2cshwcshw  12704  scshwfzeqfzo  12705  relexpsucnnr  12862  relexprelg  12873  rtrclreclem3  12895  shftfval  12905  sgnval  12923  sqrlem6  13083  summo  13541  fsum  13544  telfsumo  13618  infcvgaux1i  13670  infcvgaux2i  13671  mertenslem1  13695  mertenslem2  13696  mertens  13697  prodmo  13745  fprod  13750  ruclem12  13976  divalg  14063  ndvdssub  14067  sadcp1  14107  smupp1  14132  gcdval  14148  bezoutlem1  14178  bezoutlem3  14180  bezoutlem4  14181  bezout  14182  dvdsprime  14232  nprm  14233  dvdsprm  14242  coprm  14243  qnumval  14272  qdenval  14273  m1dvdsndvds  14327  reumodprminv  14331  pcval  14370  pceu  14372  pczpre  14373  pcdiv  14378  4sqlem2  14469  4sqlem4  14472  4sqlem12  14476  4sq  14484  vdwapval  14493  vdwapun  14494  vdwlem6  14506  cshwrepswhash1  14589  acsfn  15066  initoid  15401  termoid  15402  posi  15696  gsumval2a  16023  mgm2nsgrplem2  16154  mgm2nsgrplem3  16155  sgrp2nmndlem5  16164  mgmnsgrpex  16166  sgrpnmndex  16167  ghmf1  16412  conjnmzb  16418  orbsta  16468  symgextfv  16560  symgextfo  16564  symgfixfo  16581  pmtrprfval  16629  pmtrprfvalrn  16630  psgneu  16648  psgnval  16649  psgnvali  16650  psgnvalii  16651  odval  16675  dfod2  16703  submod  16706  isslw  16745  sylow2alem1  16754  sylow3lem2  16765  lsmelvalm  16788  lsmdisj2  16817  efgrelexlemb  16885  frgpup3lem  16912  cyggeninv  17003  cygabl  17010  gsumval3eu  17024  gsumval3OLD  17025  gsumval3lem2  17027  gsummpt1n0  17106  nn0gsumfz  17125  dprddisj2  17200  dprddisj2OLD  17201  dpjrid  17224  pgpfac1lem3  17241  f1rhm0to0ALT  17503  abveq0  17588  abvtrivd  17602  lss1d  17722  lspsn  17761  lspsnel  17762  lspprel  17853  rrgeq0i  18050  domneq0  18059  psrlidm  18169  psrlidmOLD  18170  psrridm  18171  psrridmOLD  18172  mvrval2  18191  mvrf1  18194  mplmonmul  18239  evlslem3  18296  coe1tm  18427  coe1tmfv2  18429  cply1coe0  18454  cply1coe0bi  18455  gsummoncoe1  18459  prmirredlem  18623  znf1o  18681  znfld  18690  znunit  18693  cygznlem3  18699  psgndif  18729  ipeq0  18764  obsip  18843  frlmphl  18901  uvcvval  18906  ellspd  18922  mamufacex  18976  mat1comp  19027  mat1dimelbas  19058  mat1dimid  19061  scmatel  19092  scmateALT  19099  mavmulsolcl  19138  marrepeval  19150  marepveval  19155  mdetunilem8  19206  maducoeval2  19227  madugsum  19230  minmar1eval  19236  symgmatr01lem  19240  symgmatr01  19241  gsummatr01lem3  19244  gsummatr01lem4  19245  gsummatr01  19246  m2cpm  19327  m2cpminvid2lem  19340  decpmatid  19356  monmatcollpw  19365  pmatcollpw3fi1lem1  19372  mp2pm2mplem4  19395  fvmptnn04ifc  19438  chfacffsupp  19442  chfacfscmul0  19444  chfacfscmulgsum  19446  chfacfpmmul0  19448  chfacfpmmulgsum  19450  cpmadumatpoly  19469  cayleyhamilton  19476  cayleyhamiltonALT  19477  eltopspOLD  19504  istpsOLD  19506  istopon  19511  fctop  19590  cctop  19592  ppttop  19593  pptbas  19594  epttop  19595  t0sep  19911  t1sep2  19956  cmpsublem  19985  cmpsub  19986  unisngl  20113  txuni2  20151  elpt  20158  ptbasfi  20167  xkoopn  20175  ptpjopn  20198  ptclsg  20201  dfac14lem  20203  ptcnp  20208  ptrescn  20225  tx1stc  20236  qtopeu  20302  kqt0lem  20322  isr0  20323  hauspwpwf1  20573  xmeteq0  20926  imasf1oxmet  20963  comet  21101  stdbdxmet  21103  met2ndci  21110  prdsxmslem2  21117  nrmmetd  21180  tngngp  21253  xrsxmet  21399  iccpnfcnv  21529  iccpnfhmeo  21530  cnheibor  21540  elovolm  21971  ovolgelb  21976  ovolicc1  22012  ovolicc  22019  ioorval  22068  uniioombllem6  22082  dyadmax  22092  dyadmbl  22094  i1fadd  22187  i1fmul  22188  itg1addlem3  22190  i1fmulc  22195  itg2l  22221  itg2leub  22226  limcmpt  22372  limcco  22382  dvcobr  22434  deg1ldg  22577  ig1pval  22658  elply  22677  elply2  22678  coeval  22705  coe1termlem  22740  coe1term  22741  quotval  22773  plydivlem4  22777  plydivex  22778  vieta1  22793  aannenlem2  22810  aalioulem2  22814  abelthlem9  22920  logtayllem  23127  logtayl  23128  isosctrlem2  23269  leibpilem2  23388  rlimcnp2  23413  efrlim  23416  dvdsmulf1o  23587  perfectlem2  23622  lgsfval  23693  lgsval2lem  23698  lgsdchrval  23739  2sqlem2  23756  2sqlem8  23764  2sqlem9  23765  2sqlem11  23767  dchrisum0flblem1  23810  padicval  23919  padicabv  23932  ostth1  23935  axtgcgrid  23977  axtgbtwnid  23980  islmib  24273  axpaschlem  24364  axlowdimlem15  24380  axlowdim  24385  cusgrafilem2  24601  cusgrafi  24603  wlkntrllem3  24684  fargshiftf1  24758  fargshiftfo  24759  constr3trllem2  24772  wwlkn0  24810  wlklniswwlkn1  24820  2wlkeq  24828  clwlkisclwwlklem2a1  24900  clwwlknscsh  24940  eleclclwwlkn  24954  hashecclwwlkn1  24955  usghashecclwwlk  24956  vdusgraval  25028  rusgranumwlkl1  25068  frgra3vlem1  25121  3vfriswmgralem  25125  frgrancvvdeqlem4  25154  2spotiundisj  25183  usgreghash2spotv  25187  frgregordn0  25191  numclwlk1lem2f1  25215  frgrareggt1  25237  gxval  25377  gxdi  25415  ismgmOLD  25439  nvz  25689  nmosetn0  25797  nmoolb  25803  nmoubi  25804  nmlno0lem  25825  nmlno0i  25826  hvsubeq0  26102  hvaddcan  26104  normsub0  26170  norm1exi  26285  pjhval  26432  omlsii  26438  omlsi  26439  pjoml  26471  h1de2ci  26591  spansneleq  26605  h1datomi  26616  h1datom  26617  spansncv  26688  5oalem6  26694  pj11  26749  nmopsetn0  26900  nmfnsetn0  26913  nmoplb  26942  nmopub  26943  nmfnlb  26959  nmfnleub  26960  nmlnop0iALT  27030  nmlnop0  27033  lnopeq  27044  nmopun  27049  nmcexi  27061  branmfn  27140  pjnmopi  27183  pj3i  27243  atss  27381  atom1d  27388  chirred  27430  cdj3lem2  27470  elabreximd  27526  disjxpin  27577  disjunsn  27583  br8d  27597  fmptcof2  27643  sgnsval  27871  xrge0iifcnv  28069  xrge0iifcv  28070  xrge0iifhom  28073  xrge0tmdOLD  28081  xrge0tmd  28082  esumc  28199  sgn3da  28663  sgnmul  28664  sgnnbi  28667  sgnpbi  28668  sgn0bi  28669  plymulx0  28687  signspval  28692  sconpi1  28873  cvmlift3lem2  28954  ghomf1olem  29223  br8  29351  br6  29352  br4  29353  rdgprc0  29391  dfrdg2  29393  sltval2  29581  sltintdifex  29588  sltres  29589  dfbigcup2  29702  elsingles  29721  dfiota3  29726  brimageg  29730  brdomaing  29738  brrangeg  29739  dfrdg4  29753  tfrqfree  29754  elaltxp  29778  funtransport  29834  fvtransport  29835  brsegle  29911  funray  29943  fvray  29944  funline  29945  fvline  29947  ellines  29955  linethru  29956  rankeq1o  29981  fin2so  30205  supaddc  30206  supadd  30207  ptrest  30213  heicant  30214  mblfinlem2  30217  mblfinlem3  30218  mblfinlem4  30219  ismblfin  30220  itg2addnclem  30232  itg2addnclem3  30234  itg2addnc  30235  ftc1anc  30264  subtr  30298  subtr2  30299  nn0prpw  30307  unirep  30369  f1opr  30381  sdclem2  30401  sdclem1  30402  sdc  30403  fdc  30404  isbnd  30442  heibor1lem  30471  heiborlem4  30476  heiborlem6  30478  heiborlem10  30482  maxidlmax  30606  prnc  30630  isfldidl  30631  dmnnzd  30638  elrfi  30792  nacsfg  30803  mzpcompact2lem  30849  eldioph2b  30861  eldioph3  30864  eldiophss  30873  diophrex  30874  elnn0rabdioph  30902  rencldnfilem  30919  elpell1qr  30948  elpell14qr  30950  elpell1234qr  30952  divalgmodcl  31095  jm2.27  31116  rmydioph  31122  expdiophlem2  31130  wepwsolem  31153  aomclem6  31171  lnr2i  31233  lpirlnr  31234  hbtlem2  31241  hbtlem4  31243  hbtlem5  31245  rngunsnply  31290  flcidc  31291  lcmval  31366  pm13.192  31485  refsum2cnlem1  31579  elabrexg  31597  upbdrech  31671  ssfiunibd  31675  iccshift  31724  iooshift  31728  limcperiod  31800  cncfshiftioo  31861  itgiccshift  31945  itgperiod  31946  stoweidlem46  31994  fourierdlem29  32084  fourierdlem37  32092  fourierdlem48  32103  fourierdlem51  32106  fourierdlem54  32109  fourierdlem62  32117  fourierdlem79  32134  fourierdlem81  32136  fourierdlem82  32137  fourierdlem92  32147  fourierdlem96  32151  fourierdlem97  32152  fourierdlem98  32153  fourierdlem99  32154  fourierdlem103  32158  fourierdlem104  32159  fourierdlem105  32160  fourierdlem108  32163  fourierdlem110  32165  fourierdlem112  32167  etransclem1  32184  etransclem5  32188  etransclem17  32200  etransclem32  32215  etransclem41  32224  afv0fv0  32400  afvfv0bi  32403  afvelrnb  32414  afvelrnb0  32415  mod2eq1n2dvds  32462  m1expevenALTV  32490  odd2np1ALTV  32516  opoeALTV  32525  opeoALTV  32526  perfectALTVlem2  32544  pfx2  32587  otiunsndisjX  32622  2ffzoeq  32661  usgedgnlp  32728  usgedgvadf1  32733  usgedgvadf1ALT  32736  0nodd  32816  1odd  32817  2nodd  32818  0even  32937  1neven  32938  2even  32939  2zlidl  32940  2zrngamgm  32945  2zrngagrp  32949  2zrngmmgm  32952  2zrngnmrid  32956  suppmptcfin  33172  lcoval  33213  linc0scn0  33224  linc1  33226  el0ldep  33267  snlindsntor  33272  blenval  33392  nn0sumshdiglemB  33441  equncomVD  34015  csbingVD  34031  csbsngVD  34040  csbfv12gALTVD  34046  relopabVD  34048  bnj1468  34251  riotasvd  35100  lshpdisj  35125  lsat0cv  35171  lcvexchlem4  35175  lcvexchlem5  35176  lshpkrlem1  35248  lshpkrlem2  35249  lshpkrlem3  35250  lshpkrcl  35254  islshpkrN  35258  atnle  35455  glbconxN  35515  isline  35876  ispointN  35879  pmapglbx  35906  ispsubcl2N  36084  lhp2atnle  36170  cdleme43fsv1snlem  36559  cdleme40v  36608  cdlemkid5  37074  cdlemkid  37075  dvhb1dimN  37125  dib1dim  37305  dicopelval  37317  dicelval1sta  37327  diclspsn  37334  dihvalcqpre  37375  dihglblem2aN  37433  dihglblem2N  37434  dih1dimatlem  37469  dihpN  37476  dochfl1  37616  lcfl7N  37641  lcf1o  37691  hvmapvalvalN  37901  hdmapval2lem  37974  brtrclfv2  38258  frege55lem1c  38415  frege104  38466
  Copyright terms: Public domain W3C validator