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

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

Proof of Theorem eqeq2
StepHypRef Expression
1 id 22 . 2  |-  ( A  =  B  ->  A  =  B )
21eqeq2d 2416 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-cleq 2394
This theorem is referenced by:  eqeq2i  2420  eqeq12  2421  eleq1OLD  2476  neeq2OLD  2687  alexeqg  3178  alexeq  3179  pm13.183  3190  eqeu  3220  moeq3  3226  mo2icl  3228  mob2  3229  euind  3236  reu6i  3240  reu2eqd  3246  reuind  3253  sbc2or  3286  sbc5  3302  csbiebg  3396  eqif  3923  sneq  3982  preqr1  4146  prel12  4149  preq12bg  4151  prel12g  4152  disji2  4382  disjprg  4391  dtruALT  4623  dtruALT2  4635  opth  4665  euotd  4691  solin  4767  ideqg  4975  resieq  5104  cnveqb  5279  cnveq0  5280  ordequn  5510  iota5  5553  funopg  5601  fneq2  5651  foeq3  5776  tz6.12f  5867  funbrfv  5887  fnbrfvb  5889  fvelimab  5905  elrnrexdm  6013  fconst5  6109  eufnfv  6127  f1veqaeq  6149  isosolem  6226  mpt2eq123  6337  ovmpt4g  6406  ov3  6420  ovg  6422  caovcang  6457  caovcan  6460  tfisi  6676  tfindsg  6678  findsg  6711  f1oweALT  6768  seqomlem2  7153  oawordeu  7241  omopth  7344  ereq2  7356  qsdisj  7425  eroveu  7443  2dom  7626  fundmen  7627  xpf1o  7717  nneneq  7738  cantnflem1  8140  cantnflem1OLD  8163  alephfp  8521  dfac5  8541  cardcf  8664  cfeq0  8668  sornom  8689  fpwwe2cbv  9038  fpwwe2lem3  9041  ltsosr  9501  map2psrpr  9517  axpre-lttri  9572  subval  9847  divval  10250  nn0ind-raph  11003  uzrdgfni  12110  sqeqor  12326  nn0opth2  12396  hashrabsn1  12490  elprchashprn2  12510  hashbclem  12550  hashbc  12551  hash2prde  12565  hash2pwpr  12568  wrdind  12758  wrd2ind  12759  reuccats1lem  12761  relexpindlem  13045  sqrtval  13219  sqrmo  13234  summolem2  13687  prodmolem2  13894  divides  14197  dvdstr  14227  odd2np1lem  14254  ndvdssub  14274  bitsinv1  14301  eucalglt  14423  ramcl2lem  14736  ramcl  14756  cshwrepswhash1  14796  imasaddfnlem  15142  fnhomeqhomf  15304  initoeu2lem1  15617  posi  15903  sgrp2nmndlem3  16367  orbsta  16675  symgfvne  16737  symgfix2  16765  odlem1  16883  gexlem1  16923  slwispgp  16955  sylow3lem6  16976  efgrelexlemb  17092  gsumval3OLD  17232  gsumval3lem2  17234  pgpfac1  17451  pgpfaclem2  17453  pgpfac  17455  ablfaclem1  17456  isdomn  18263  mvrval  18397  coe1tmmul2  18637  coe1tmmul  18638  obsip  19050  uvcval  19112  mat1comp  19234  mat1dimid  19268  scmateALT  19306  marrepval  19356  marepvval  19361  minmar1val  19442  gsummatr01  19453  t0sep  20118  t1sep2  20163  is2ndc  20239  kqt0lem  20529  isr0  20530  isufil2  20701  xmeteq0  21133  imasf1oxmet  21170  xrsxmet  21606  iccpnfcnv  21736  dyadmax  22299  dyadmbl  22301  dvfsumle  22714  dvfsumabs  22716  dvfsumlem1  22719  mdegle0  22769  fta1g  22860  ig1peu  22864  fta1  22996  aalioulem2  23021  efopn  23333  efrlim  23625  musum  23848  dvdsmulf1o  23851  dchrsum2  23924  sumdchr2  23926  axtgcgrid  24239  axtgbtwnid  24242  tglowdim1i  24273  islmib  24543  axcontlem12  24695  wlkon  24950  wlkntrllem3  24980  spthonepeq  25006  fargshiftf1  25054  constr3trllem2  25068  wlklniswwlkn2  25117  usg2wlkeq  25125  wwlknredwwlkn  25143  wwlkextprop  25161  clwwlkn  25184  clwlkisclwwlklem2a4  25201  clwwlkext2edg  25219  clwwnisshclwwn  25226  hashecclwwlkn1  25251  usghashecclwwlk  25252  clwlkfoclwwlk  25262  2wlkonot  25282  2spthonot  25283  el2wlkonot  25286  el2spthonot  25287  el2spthonot0  25288  rusgraprop2  25359  rusgrasn  25362  rusgranumwlklem1  25366  rusgranumwlklem2  25367  rusgranumwlklem3  25368  rusgranumwlkg  25375  clwlknclwlkdifs  25377  frgra3vlem1  25417  3vfriswmgralem  25421  usg2spot2nb  25482  usgreg2spot  25484  2spotmdisj  25485  usgreghash2spot  25486  numclwwlkdisj  25497  numclwwlkovf  25498  numclwwlkovg  25504  numclwlk1lem2f1  25511  numclwwlkovq  25516  numclwwlkovh  25518  numclwwlk5  25529  frgrareg  25534  frgraregord013  25535  friendshipgt3  25538  ex-opab  25570  isgrpoi  25614  grpoidinv2  25634  isgrp2d  25651  isgrpda  25713  isexid2  25741  ghgrpOLD  25784  hvsubeq0  26399  hvaddcan  26401  hvsubadd  26408  normsub0  26467  omlsi  26736  pjoml  26768  nonbooli  26983  pj11  27046  lnopeq  27341  nmopun  27346  pjclem4a  27530  pj3lem1  27538  strlem4  27586  hstrlem4  27594  jplem1  27600  superpos  27686  rmoeq  27801  ifeqeqx  27840  disji2f  27869  disjif2  27873  disjabrex  27874  disjabrexf  27875  disjxpin  27880  disjunsn  27886  ofpreima  27950  fgreu  27956  fcnvgreu  27957  xrge0iifcnv  28368  esumpr2  28514  eulerpartlemgvv  28821  eulerpartlemgh  28823  eulerpartlemgs2  28825  sgnsub  28989  plymulx0  29010  bnj1321  29410  subfacp1lem3  29479  pconcn  29521  cnpcon  29527  txpcon  29529  conpcon  29532  cvmlift3lem2  29617  cvmlift3lem4  29619  cvmlift3  29625  snmlflim  29629  ghomf1olem  29886  iota5f  29931  br1steqg  29989  br2ndeqg  29990  sltres  30124  nofulllem5  30166  rankeq1o  30509  nn0prpw  30551  bj-csbsnlem  31034  fin2so  31412  mblfinlem2  31424  mbfresfi  31433  cnambfre  31435  ftc1anclem8  31470  f1opr  31497  fdc  31520  istotbnd  31547  ismaxidl  31719  mpt2bi123f  31853  mptbi12f  31857  lsatcmp  32021  lshpkrlem1  32128  trlval2  33181  cdlemg1cex  33607  cdlemm10N  34138  dicval  34196  unxpwdom3  35403  dgraalem  35458  dgraaub  35461  hashgcdeq  35522  frege104  35948  pm13.192  36165  2sbc6g  36170  2sbc5g  36171  pm14.122b  36178  equncomVD  36699  csbingVD  36715  csbsngVD  36724  csbxpgVD  36725  csbresgVD  36726  csbrngVD  36727  csbima12gALTVD  36728  csbunigVD  36729  csbfv12gALTVD  36730  relopabVD  36732  dvnprodlem1  37111  dvnprodlem2  37112  dvnprodlem3  37113  dvnprod  37114  fourierdlem42  37299  etransclem11  37396  etransclem12  37397  etransclem33  37418  reuccatpfxs1lem  37920  lidldomn1  38238  nn0sumshdiglem2  38753
  Copyright terms: Public domain W3C validator