MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reseq2d Structured version   Visualization version   GIF version

Theorem reseq2d 5301
Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
reseq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem reseq2d
StepHypRef Expression
1 reseqd.1 . 2 (𝜑𝐴 = 𝐵)
2 reseq2 5296 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cres 5027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-in 3543  df-opab 4635  df-xp 5031  df-res 5037
This theorem is referenced by:  reseq12d  5302  resima2OLD  5337  relresfld  5562  f1orescnv  6047  fococnv2  6057  fvn0ssdmfun  6240  fnressn  6305  fnsnsplit  6330  oprssov  6675  curry1  7130  curry2  7133  dftpos2  7230  wrecseq123  7269  wfr3g  7274  wfrlem1  7275  wfrlem4  7279  wfrlem14  7289  wfr2a  7293  dfrecs3  7330  tfrlem16  7350  tfr2ALT  7358  tfr3ALT  7359  sbthlem4  7932  mapunen  7988  hartogslem1  8304  axdc3lem2  9130  fseq1p1m1  12235  hashf1lem1  13045  relexp0g  13553  relexp0  13554  relexpsucnnr  13556  dfrtrcl2  13593  bpolylem  14561  setsval  15663  idfuval  16302  idfu2nd  16303  resf1st  16320  setcid  16502  catcisolem  16522  estrcid  16540  funcestrcsetclem5  16550  funcsetcestrclem5  16565  funcsetcestrclem7  16567  1stfval  16597  1stf2  16599  2ndfval  16600  2ndf2  16602  1stfcl  16603  2ndfcl  16604  curf2ndf  16653  hofcl  16665  isps  16968  cnvps  16978  isdir  16998  dirref  17001  tsrdir  17004  frmdval  17154  frmdplusg  17157  gsum2dlem2  18136  dprd2da  18207  dpjval  18221  ablfac1eulem  18237  ablfac1eu  18238  psrplusg  19145  opsrtoslem2  19249  mdetunilem3  20178  mdetunilem4  20179  mdetunilem9  20184  imacmp  20949  ptuncnv  21359  tgphaus  21669  tsmsres  21696  tsmsxplem1  21705  tsmsxplem2  21706  trust  21782  metreslem  21915  imasdsf1olem  21926  xmspropd  22026  mspropd  22027  imasf1oxms  22042  imasf1oms  22043  nmpropd2  22147  isngp2  22149  ngppropd  22186  tngngp2  22201  cmspropd  22868  mbfres2  23132  limciun  23378  dvmptres3  23439  dvmptres2  23445  dvmptntr  23454  dvlipcn  23475  dvlip2  23476  c1liplem1  23477  dvgt0lem1  23483  lhop1lem  23494  dvcnvrelem1  23498  dvcvx  23501  ftc2ditglem  23526  wilthlem2  24509  dchrval  24673  dchrelbas2  24676  ausisusgraedg  25648  1pthonlem1  25882  constr2pth  25894  eupath2lem3  26269  eupath2  26270  hhssablo  27307  hhssnvt  27309  hhsssh  27313  resf1o  28696  gsummpt2d  28915  qtophaus  29034  esumcvg  29278  eulerpartlemn  29573  sseqp1  29587  signsvtn0  29776  bnj1385  29960  bnj1326  30151  bnj1321  30152  bnj1442  30174  bnj1450  30175  bnj1463  30180  bnj1529  30195  cvmliftlem5  30328  cvmliftlem7  30330  cvmliftlem10  30333  cvmliftlem11  30334  cvmliftlem15  30337  cvmlift2lem11  30352  cvmlift2lem12  30353  eldm3  30708  funsseq  30715  frr3g  30826  frrlem1  30827  frrlem4  30830  finixpnum  32364  poimirlem3  32382  poimirlem4  32383  poimirlem9  32388  sdclem2  32508  prdsbnd2  32564  isdivrngo  32719  drngoi  32720  dibffval  35247  hdmapffval  35936  hdmapfval  35937  eldiophb  36138  diophrw  36140  diophin  36154  rclexi  36741  rtrclex  36743  rtrclexi  36747  cnvrcl0  36751  dfrtrcl5  36755  dfrcl2  36785  fvmptiunrelexplb0da  36796  sblpnf  37331  fresin2  38147  cncfuni  38573  dvresntr  38607  dvbdfbdioolem1  38619  itgiccshift  38673  itgperiod  38674  dirkercncflem2  38798  fourierdlem46  38846  fourierdlem48  38848  fourierdlem49  38849  fourierdlem58  38858  fourierdlem72  38872  fourierdlem74  38874  fourierdlem75  38875  fourierdlem81  38881  fourierdlem88  38888  fourierdlem89  38889  fourierdlem90  38890  fourierdlem91  38891  fourierdlem92  38892  fourierdlem103  38903  fourierdlem104  38904  fourierdlem112  38912  fouriersw  38925  voncmpl  39312  funcoressn  39657  resresdm  40131  resunimafz0  40192  egrsubgr  40500  pthdlem1  40971  eupthvdres  41402  eupth2lem3  41403  eupth2  41406  eucrct2eupth  41412  idfusubc0  41654  idfusubc  41655  rngcval  41753  rnghmsubcsetclem1  41766  rngccat  41769  rngcid  41770  rngcidALTV  41782  rngcifuestrc  41788  funcrngcsetc  41789  funcrngcsetcALT  41790  ringcval  41799  rhmsubcsetclem1  41812  ringccat  41815  ringcid  41816  rhmsubcrngclem1  41818  rhmsubcrngc  41820  funcringcsetc  41826  funcringcsetcALTV2lem5  41831  ringcidALTV  41845  funcringcsetclem5ALTV  41854  rhmsubc  41881  rhmsubcALTVlem3  41898  aacllem  42316
  Copyright terms: Public domain W3C validator