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

Theorem reseq2d 5831
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 5826 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cres 5534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-rab 3139  df-in 3915  df-opab 5105  df-xp 5538  df-res 5544
This theorem is referenced by:  reseq12d  5832  resresdm  6068  relresfld  6105  f1orescnv  6612  fococnv2  6622  fvn0ssdmfun  6824  fnressn  6902  fnsnsplit  6928  oprssov  7302  curry1  7786  curry2  7789  dftpos2  7896  wrecseq123  7935  wfr3g  7940  wfrlem1  7941  wfrlem4  7945  wfrlem14  7955  wfr2a  7959  dfrecs3  7996  tfrlem16  8016  tfr2ALT  8024  tfr3ALT  8025  sbthlem4  8618  mapunen  8674  hartogslem1  8994  axdc3lem2  9862  fseq1p1m1  12976  resunimafz0  13799  hashf1lem1  13809  relexp0g  14372  relexp0  14373  relexpsucnnr  14375  dfrtrcl2  14412  bpolylem  15393  setsval  16504  idfuval  17137  idfu2nd  17138  resf1st  17155  setcid  17337  catcisolem  17357  estrcid  17375  funcestrcsetclem5  17385  funcsetcestrclem5  17400  funcsetcestrclem7  17402  1stfval  17432  1stf2  17434  2ndfval  17435  2ndf2  17437  1stfcl  17438  2ndfcl  17439  curf2ndf  17488  hofcl  17500  isps  17803  cnvps  17813  isdir  17833  dirref  17836  tsrdir  17839  frmdval  18007  frmdplusg  18010  gsum2dlem2  19082  dprd2da  19155  dpjval  19169  ablfac1eulem  19185  ablfac1eu  19186  psrplusg  20617  opsrtoslem2  20722  mdetunilem3  21217  mdetunilem4  21218  mdetunilem9  21223  imacmp  22000  ptuncnv  22410  tgphaus  22720  tsmsres  22747  tsmsxplem1  22756  tsmsxplem2  22757  trust  22833  metreslem  22967  imasdsf1olem  22978  xmspropd  23078  mspropd  23079  imasf1oxms  23094  imasf1oms  23095  nmpropd2  23199  isngp2  23201  ngppropd  23241  tngngp2  23256  cphsscph  23853  cmspropd  23951  cmssmscld  23952  mbfres2  24247  limciun  24495  dvmptres3  24557  dvmptres2  24563  dvmptntr  24572  dvlipcn  24595  dvlip2  24596  c1liplem1  24597  dvgt0lem1  24603  lhop1lem  24614  dvcnvrelem1  24618  dvcvx  24621  ftc2ditglem  24646  wilthlem2  25652  dchrval  25816  dchrelbas2  25819  egrsubgr  27065  pthdlem1  27553  eupthvdres  28018  eupth2lem3  28019  eupth2  28022  eucrct2eupth  28028  hhssablo  29044  hhssnvt  29046  hhsssh  29050  fnunres1  30364  resf1o  30476  gsummpt2d  30718  symgcom  30758  tocycval  30781  tocycfv  30782  tocycf  30790  tocyc01  30791  cycpm2tr  30792  cycpmconjslem1  30827  cycpmconjslem2  30828  qtophaus  31158  esumcvg  31419  eulerpartlemn  31713  sseqp1  31727  signsvtn0  31914  ftc2re  31943  reprsuc  31960  bnj1385  32178  bnj1326  32372  bnj1321  32373  bnj1442  32395  bnj1450  32396  bnj1463  32401  bnj1529  32416  f1resfz0f1d  32435  pfxwlk  32444  pthhashvtx  32448  cvmliftlem5  32610  cvmliftlem7  32612  cvmliftlem10  32615  cvmliftlem11  32616  cvmliftlem15  32619  cvmlift2lem11  32634  cvmlift2lem12  32635  satffunlem1lem1  32723  satffunlem2lem1  32725  eldm3  33071  funsseq  33085  frecseq123  33193  frr3g  33195  fpr3g  33196  frrlem1  33197  frrlem4  33200  frrlem12  33208  fpr2  33214  frr2  33219  noresle  33274  nosupno  33277  nosupdm  33278  nosupfv  33280  nosupres  33281  nosupbnd1lem1  33282  nosupbnd1lem3  33284  nosupbnd1lem5  33286  nosupbnd1  33288  nosupbnd2  33290  noeta  33296  finixpnum  35000  poimirlem3  35018  poimirlem4  35019  poimirlem9  35024  sdclem2  35138  prdsbnd2  35191  isdivrngo  35346  drngoi  35347  elrefsymrels2  35923  eleqvrels2  35945  dibffval  38394  hdmapffval  39080  hdmapfval  39081  eldiophb  39628  diophrw  39630  diophin  39643  rclexi  40245  rtrclex  40247  rtrclexi  40251  cnvrcl0  40255  dfrtrcl5  40259  dfrcl2  40305  fvmptiunrelexplb0da  40316  sblpnf  40948  fresin2  41733  limsupresuz  42284  limsupvaluz  42289  limsupvaluz2  42319  supcnvlimsup  42321  climrescn  42329  liminfresuz  42365  cncfuni  42467  dvresntr  42499  dvbdfbdioolem1  42509  itgiccshift  42561  itgperiod  42562  dirkercncflem2  42685  fourierdlem46  42733  fourierdlem48  42735  fourierdlem49  42736  fourierdlem58  42745  fourierdlem72  42759  fourierdlem74  42761  fourierdlem75  42762  fourierdlem81  42768  fourierdlem88  42775  fourierdlem89  42776  fourierdlem90  42777  fourierdlem91  42778  fourierdlem92  42779  fourierdlem103  42790  fourierdlem104  42791  fourierdlem112  42799  fouriersw  42812  voncmpl  43199  funcoressn  43573  funressnmo  43577  funressndmafv2rn  43718  f1oresf1orab  43784  isomgreqve  44282  idfusubc0  44428  idfusubc  44429  rngcval  44525  rnghmsubcsetclem1  44538  rngccat  44541  rngcid  44542  rngcidALTV  44554  rngcifuestrc  44560  funcrngcsetc  44561  funcrngcsetcALT  44562  ringcval  44571  rhmsubcsetclem1  44584  ringccat  44587  ringcid  44588  rhmsubcrngclem1  44590  rhmsubcrngc  44592  funcringcsetc  44598  funcringcsetcALTV2lem5  44603  ringcidALTV  44617  funcringcsetclem5ALTV  44626  rhmsubc  44653  rhmsubcALTVlem3  44669  itcoval  45014  itcoval0mpt  45019  itcovalendof  45022  aacllem  45268
  Copyright terms: Public domain W3C validator