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

Theorem eqeq1 2455
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 2453 1  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-cleq 2443
This theorem is referenced by:  eqeq1i  2458  eqeq2OLD  2467  eqeq12  2470  eqtr  2477  eqsb3lem  2570  clelab  2595  clelabOLD  2596  neeq1OLD  2730  pm13.18  2759  issetf  3073  sbhypf  3115  vtoclgft  3116  rexraleqim  3182  eqvincf  3184  pm13.183  3197  eueq  3228  mob  3238  euind  3243  reu2eqd  3253  reuind  3260  eqsbc3  3324  csbhypf  3405  uniiunlem  3538  snjust  3974  elprg  3991  elsncg  3998  rabrsn  4043  sneqrg  4140  preq12bg  4149  prel12g  4150  intab  4256  uniintsn  4263  dfiin2g  4301  disji2  4377  disjprg  4386  eusv1  4584  reusv2lem2  4592  reusv3  4598  reusv6OLD  4601  opthg  4665  copsexg  4674  copsexgOLD  4675  euotd  4690  elopab  4695  solin  4762  elxpi  4954  opbrop  5014  relop  5088  ideqg  5089  elrnmpt  5184  elrnmpt1  5186  elrnmptg  5187  somin1  5332  cnveqb  5391  relcoi1  5464  funopg  5548  fvelrnb  5838  fvmptg  5871  fndmin  5909  eldmrexrn  5948  foelrn  5961  foco2  5962  fmptco  5975  fmptsng  5999  eufnfv  6050  elabrex  6059  abrexco  6060  f1veqaeq  6071  isosolem  6137  f1oiso  6141  eusvobj2  6183  oprabid  6214  mpt2fun  6292  elrnmpt2g  6302  elrnmpt2  6303  elrnmpt2res  6304  ralrnmpt2  6305  ov3  6327  ov6g  6328  ovelrn  6339  caovcang  6364  caovcan  6367  snnex  6482  uniuni  6485  orduninsuc  6554  funcnvuni  6630  fun11iun  6637  f1oweALT  6661  opiota  6733  eloprabi  6736  frxp  6782  funsssuppss  6815  dftpos4  6864  tz7.44-2  6963  tz7.44-3  6964  oev  7054  oalimcl  7099  omlimcl  7117  odi  7118  omeu  7124  oeeui  7141  nneob  7191  omopth  7197  elqsg  7252  qsdisj  7277  qsel  7279  brecop  7293  eroveu  7295  erovlem  7296  th3qlem1  7306  th3q  7309  elixpsn  7402  ixpsnf1o  7403  boxcutc  7406  2dom  7482  fundmen  7483  xpf1o  7573  nneneq  7594  fofinf1o  7693  elfi  7764  elfiun  7781  dffi3  7782  brwdom  7883  brwdom3  7898  unwdomg  7900  xpwdomg  7901  noinfep  7966  cantnfp1lem1  7987  cantnfp1lem3  7989  cantnflem1  7998  cantnfp1lem1OLD  8013  cantnfp1lem3OLD  8015  cantnfp1OLD  8016  cantnflem1OLD  8021  scott0  8194  carden2a  8237  cardiun  8253  pm54.43lem  8270  alephval3  8381  dfac5lem3  8396  dfac5lem4  8397  dfac2  8401  kmlem9  8428  kmlem12  8431  cardcf  8522  cfeq0  8526  cfsuc  8527  cff1  8528  cflim2  8533  cfss  8535  isfin5  8569  fin1a2lem11  8680  fin1a2lem13  8682  brdom7disj  8799  brdom6disj  8800  canthp1lem2  8921  canthp1  8922  tskuni  9051  gruina  9086  genpv  9269  genpelv  9270  ltsosr  9362  ltresr  9408  axcnre  9432  axpre-lttri  9433  ltordlem  9966  ltord1  9967  fimaxre3  10380  supmul1  10396  supmullem1  10397  supmullem2  10398  supmul  10399  creur  10417  creui  10418  nn1m1nn  10443  elz  10749  nn0ind-raph  10843  xnegeq  11278  xmullem2  11329  xmulasslem  11349  fleqceilz  11794  fseqsupubi  11901  sqeqor  12081  nn0opth2  12151  hash1snb  12273  euhash1  12274  hash2prde  12281  hash2prd  12283  hash2pwpr  12284  brfi1uzind  12321  wrd2ind  12474  cshfn  12529  ccatco  12565  shftfval  12661  sgnval  12679  sqrlem6  12839  summo  13296  fsum  13299  fsumtscopo  13367  infcvgaux1i  13421  infcvgaux2i  13422  mertenslem1  13446  mertenslem2  13447  mertens  13448  ruclem12  13625  divalg  13709  ndvdssub  13713  bitsinvp1  13747  sadcp1  13753  smupp1  13778  gcdval  13794  bezoutlem1  13824  bezoutlem3  13826  bezoutlem4  13827  bezout  13828  dvdsprime  13878  nprm  13879  dvdsprm  13887  coprm  13888  qnumval  13917  qdenval  13918  reumodprminv  13974  pcval  14013  pceu  14015  pczpre  14016  pcdiv  14021  4sqlem2  14112  4sqlem4  14115  4sqlem12  14119  4sq  14127  vdwapval  14136  vdwapun  14137  vdwlem6  14149  cshwrepswhash1  14231  acsfn  14699  posi  15222  gsumval2a  15614  ghmf1  15877  conjnmzb  15883  orbsta  15933  symgextfv  16025  symgextfo  16029  symgfixfo  16047  pmtrprfval  16095  pmtrprfvalrn  16096  psgneu  16114  psgnval  16115  psgnvali  16116  psgnvalii  16117  odval  16141  dfod2  16169  submod  16172  isslw  16211  sylow2alem1  16220  sylow3lem2  16231  lsmelvalm  16254  lsmdisj2  16283  efgrelexlemb  16351  frgpup3lem  16378  cyggeninv  16464  cygabl  16471  gsumval3eu  16485  gsumval3OLD  16486  gsumval3lem2  16488  gsummpt1n0  16561  dprddisj2  16642  dprddisj2OLD  16643  dpjrid  16666  pgpfac1lem3  16683  f1rhm0to0ALT  16935  abveq0  17017  abvtrivd  17031  lss1d  17150  lspsn  17189  lspsnel  17190  lspprel  17281  rrgeq0i  17466  domneq0  17475  psrlidm  17580  psrlidmOLD  17581  psrridm  17582  psrridmOLD  17583  mvrval2  17602  mvrf1  17605  mplmonmul  17650  evlslem3  17707  coe1tm  17834  coe1tmfv2  17836  xrsdsreval  17967  prmirredlem  18026  prmirredlemOLD  18029  znf1o  18093  znfld  18102  znunit  18105  cygznlem3  18111  psgndif  18141  ipeq0  18176  obsip  18255  frlmphl  18315  uvcvval  18320  ellspd  18339  ellspdOLD  18340  mamufacex  18398  dmatcomp  18412  mavmulsolcl  18473  marrepeval  18485  marepveval  18490  mdetunilem8  18541  maducoeval2  18562  madugsum  18565  minmar1eval  18571  symgmatr01lem  18575  symgmatr01  18576  gsummatr01lem3  18579  gsummatr01lem4  18580  gsummatr01  18581  eltopspOLD  18639  istpsOLD  18641  istopon  18646  fctop  18724  cctop  18726  ppttop  18727  pptbas  18728  epttop  18729  t0sep  19044  t1sep2  19089  cmpsublem  19118  cmpsub  19119  txuni2  19254  elpt  19261  ptbasfi  19270  xkoopn  19278  ptpjopn  19301  ptclsg  19304  dfac14lem  19306  ptcnp  19311  ptrescn  19328  tx1stc  19339  qtopeu  19405  kqt0lem  19425  isr0  19426  hauspwpwf1  19676  xmeteq0  20029  imasf1oxmet  20066  comet  20204  stdbdxmet  20206  met2ndci  20213  prdsxmslem2  20220  nrmmetd  20283  tngngp  20356  xrsxmet  20502  iccpnfcnv  20632  iccpnfhmeo  20633  oprpiece1res2  20640  cnheibor  20643  phtpycc  20679  elovolm  21074  ovolgelb  21079  ovolicc1  21115  ovolicc  21122  ioorval  21170  uniioombllem6  21184  dyadmax  21194  dyadmbl  21196  i1fadd  21289  i1fmul  21290  itg1addlem3  21292  i1fmulc  21297  itg2l  21323  itg2leub  21328  limcmpt  21474  limcco  21484  dvcobr  21536  deg1ldg  21679  ig1pval  21760  elply  21779  elply2  21780  coeval  21807  coe1termlem  21841  coe1term  21842  quotval  21874  plydivlem4  21878  plydivex  21879  vieta1  21894  aannenlem2  21911  aalioulem2  21915  abelthlem9  22021  logtayllem  22220  logtayl  22221  isosctrlem2  22333  atantayl2  22449  leibpilem2  22452  rlimcnp2  22476  efrlim  22479  dvdsmulf1o  22650  perfectlem2  22685  lgsfval  22756  lgsval2lem  22761  lgsdchrval  22802  2sqlem2  22819  2sqlem8  22827  2sqlem9  22828  2sqlem11  22830  dchrisum0flblem1  22873  padicval  22982  padicabv  22995  ostth1  22998  axtgcgrid  23040  axtgbtwnid  23043  axpaschlem  23321  axlowdimlem15  23337  axlowdim  23342  cusgrafilem2  23523  cusgrafi  23525  wlkntrllem3  23595  fargshiftf1  23658  fargshiftfo  23659  constr3trllem2  23672  vdusgraval  23712  gxval  23880  gxdi  23918  ismgm  23942  nvz  24192  nmosetn0  24300  nmoolb  24306  nmoubi  24307  nmlno0lem  24328  nmlno0i  24329  hvsubeq0  24605  hvaddcan  24607  normsub0  24673  norm1exi  24788  pjhval  24935  omlsii  24941  omlsi  24942  pjoml  24974  h1de2ci  25094  spansneleq  25108  h1datomi  25119  h1datom  25120  spansncv  25191  5oalem6  25197  pj11  25252  nmopsetn0  25404  nmfnsetn0  25417  nmoplb  25446  nmopub  25447  nmfnlb  25463  nmfnleub  25464  nmlnop0iALT  25534  nmlnop0  25537  lnopeq  25548  nmopun  25553  nmcexi  25565  branmfn  25644  pjnmopi  25687  pj3i  25747  atss  25885  atom1d  25892  chirred  25934  cdj3lem2  25974  elabreximd  26026  disjxpin  26064  disjunsn  26070  br8d  26076  fmptcof2  26113  sgnsval  26325  xrge0iifcnv  26497  xrge0iifcv  26498  xrge0iifhom  26501  xrge0tmdOLD  26509  xrge0tmd  26510  esumc  26639  sgn3da  27058  sgnmul  27059  sgnnbi  27062  sgnpbi  27063  sgn0bi  27064  ccatmulgnn0dir  27074  plymulx0  27082  plymulx  27083  signspval  27087  sconpi1  27262  cvmlift3lem2  27343  ghomf1olem  27447  relexp0  27465  relexpsucr  27466  relexpsucl  27468  rtrclreclem.trans  27482  prodmo  27583  fprod  27588  br8  27700  br6  27701  br4  27702  rdgprc0  27741  dfrdg2  27743  sltval2  27931  sltintdifex  27938  sltres  27939  dfbigcup2  28064  elsingles  28083  dfiota3  28088  brimageg  28092  brdomaing  28100  brrangeg  28101  dfrdg4  28115  tfrqfree  28116  elaltxp  28140  funtransport  28196  fvtransport  28197  brsegle  28273  funray  28305  fvray  28306  funline  28307  fvline  28309  ellines  28317  linethru  28318  rankeq1o  28343  fin2so  28554  supaddc  28555  supadd  28556  ptrest  28563  heicant  28564  mblfinlem1  28566  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  itg2addnclem  28581  itg2addnclem3  28583  itg2addnc  28584  ftc1anc  28613  subtr  28647  subtr2  28648  nn0prpw  28656  unirep  28744  f1opr  28756  sdclem2  28776  sdclem1  28777  sdc  28778  fdc  28779  isbnd  28817  heibor1lem  28846  heiborlem4  28851  heiborlem6  28853  heiborlem10  28857  maxidlmax  28981  prnc  29005  isfldidl  29006  dmnnzd  29013  elrfi  29168  nacsfg  29179  mzpcompact2lem  29226  eldioph2b  29239  eldioph3  29242  eldiophss  29251  diophrex  29252  elnn0rabdioph  29279  rencldnfilem  29297  elpell1qr  29326  elpell14qr  29328  elpell1234qr  29330  divalgmodcl  29474  jm2.27  29495  rmydioph  29501  expdiophlem2  29509  wepwsolem  29532  aomclem6  29550  lnr2i  29610  lpirlnr  29611  hbtlem2  29618  hbtlem4  29620  hbtlem5  29622  rngunsnply  29668  flcidc  29669  pm13.192  29802  refsum2cnlem1  29897  stoweidlem46  29979  afv0fv0  30193  afvfv0bi  30196  afvelrnb  30207  afvelrnb0  30208  otiunsndisj  30270  otiunsndisjX  30271  f0rn0  30279  oprabv  30295  2ffzoeq  30352  m1dvdsndvds  30385  2wlkeq  30426  wwlkn0  30461  wlklniswwlkn1  30471  clwlkisclwwlklem2a1  30579  cshwlemma1  30627  scshwfzeqfzo  30630  Lemma2  30631  eleclclwwlkn  30645  hashecclwwlkn1  30646  usghashecclwwlk  30647  rusgranumwlkl1  30697  frgra3vlem1  30730  3vfriswmgralem  30734  frgrancvvdeqlem4  30764  2spotiundisj  30793  usgreghash2spotv  30797  frgregordn0  30801  numclwlk1lem2f1  30825  frgrareggt1  30847  fmptsnd  30860  suppmptcfin  30931  nn0gsumfz  30945  gsummoncoe1  30985  cply1coe0  30991  cply1coe0bi  30992  scmatscmids  31014  mat1dimelbas  31021  mat1dimid  31024  lcoval  31053  linc0scn0  31064  linc1  31066  el0ldep  31107  snlindsntor  31112  m2cpm  31204  m2pminv2lem  31212  pmatcollpw1id  31226  monmatcollpw  31236  pmatcollpw4fi1lem1  31242  mp2pm2mplem4  31264  fvmptnn04ifc  31306  chfacffsupp  31310  chfacfscmul0  31312  chfacfscmulgsum  31314  chfacfpmmul0  31316  chfacfpmmulgsum  31318  cpmadumatpoly  31338  cayleyhamilton  31345  cayleyhamiltonALT  31346  equncomVD  31904  csbingVD  31920  csbsngVD  31929  csbfv12gALTVD  31935  relopabVD  31937  bnj1468  32139  riotasvd  32913  lshpdisj  32938  lsat0cv  32984  lcvexchlem4  32988  lcvexchlem5  32989  lshpkrlem1  33061  lshpkrlem2  33062  lshpkrlem3  33063  lshpkrcl  33067  islshpkrN  33071  atnle  33268  glbconxN  33328  isline  33689  ispointN  33692  pmapglbx  33719  ispsubcl2N  33897  lhp2atnle  33983  cdleme43fsv1snlem  34370  cdleme40v  34419  cdlemkid5  34885  cdlemkid  34886  dvhb1dimN  34936  dib1dim  35116  dicopelval  35128  dicelval1sta  35138  diclspsn  35145  dihvalcqpre  35186  dihglblem2aN  35244  dihglblem2N  35245  dih1dimatlem  35280  dihpN  35287  dochfl1  35427  lcfl7N  35452  lcf1o  35502  hvmapvalvalN  35712  hdmapval2lem  35785
  Copyright terms: Public domain W3C validator