Theorem reseq2d 5946

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

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq2 5941	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1542   ↾ cres 5634

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910  df-opab 5163  df-xp 5638  df-res 5644

This theorem is referenced by:  reseq12d  5947  imadifssran  6117  resresdm  6199  relresfld  6242  fnunres1  6612  f1orescnv  6797  fococnv2  6808  fvn0ssdmfun  7028  fnressn  7113  fnsnsplit  7140  oprssov  7537  curry1  8056  curry2  8059  dftpos2  8195  frecseq123  8234  fpr3g  8237  frrlem1  8238  frrlem4  8241  frrlem12  8249  fpr2a  8254  wfr3g  8271  dfrecs3  8314  tfrlem16  8334  tfr2ALT  8342  tfr3ALT  8343  on2recsov  8606  sbthlem4  9030  mapunen  9086  hartogslem1  9459  frr3g  9680  frr2  9684  axdc3lem2  10373  fseq1p1m1  13526  resunimafz0  14380  hashf1lem1  14390  relexp0g  14957  relexp0  14958  relexpsucnnr  14960  dfrtrcl2  14997  bpolylem  15983  setsval  17106  idfuval  17812  idfu2nd  17813  resf1st  17830  idfusubc0  17835  idfusubc  17836  setcid  18022  catcisolem  18046  estrcid  18069  funcestrcsetclem5  18079  funcsetcestrclem5  18094  funcsetcestrclem7  18096  1stfval  18126  1stf2  18128  2ndfval  18129  2ndf2  18131  1stfcl  18132  2ndfcl  18133  curf2ndf  18182  hofcl  18194  isps  18503  cnvps  18513  isdir  18533  dirref  18536  tsrdir  18539  frmdval  18788  frmdplusg  18791  gsum2dlem2  19912  dprd2da  19985  dpjval  19999  ablfac1eulem  20015  ablfac1eu  20016  rngcval  20563  rnghmsubcsetclem1  20576  rngccat  20579  rngcid  20580  rngcifuestrc  20584  funcrngcsetc  20585  funcrngcsetcALT  20586  ringcval  20592  rhmsubcsetclem1  20605  ringccat  20608  ringcid  20609  rhmsubcrngclem1  20611  rhmsubcrngc  20613  funcringcsetc  20619  rhmsubc  20634  psrplusg  21904  opsrtoslem2  22023  mdetunilem3  22570  mdetunilem4  22571  mdetunilem9  22576  imacmp  23353  ptuncnv  23763  tgphaus  24073  tsmsres  24100  tsmsxplem1  24109  tsmsxplem2  24110  trust  24185  metreslem  24318  imasdsf1olem  24329  xmspropd  24429  mspropd  24430  imasf1oxms  24445  imasf1oms  24446  nmpropd2  24551  isngp2  24553  ngppropd  24593  tngngp2  24608  cphsscph  25219  cmspropd  25317  cmssmscld  25318  mbfres2  25614  limciun  25863  dvmptres3  25928  dvmptres2  25934  dvmptntr  25943  dvlipcn  25967  dvlip2  25968  c1liplem1  25969  dvgt0lem1  25975  lhop1lem  25986  dvcnvrelem1  25990  dvcvx  25993  ftc2ditglem  26020  wilthlem2  27047  dchrval  27213  dchrelbas2  27216  noresle  27677  nosupcbv  27682  nosupno  27683  nosupdm  27684  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem3  27690  nosupbnd1lem5  27692  nosupbnd1  27694  nosupbnd2  27696  noinfcbv  27697  noinfno  27698  noinfdm  27699  noinffv  27701  noinfres  27702  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noinfbnd1  27709  noinfbnd2  27711  noetalem1  27721  norecov  27955  norec2ov  27965  egrsubgr  29362  dfpth2  29814  pthdlem1  29851  eupthvdres  30322  eupth2lem3  30323  eupth2  30326  eucrct2eupth  30332  hhssablo  31350  hhssnvt  31352  hhsssh  31356  fresunsn  32714  fressupp  32777  resf1o  32819  gsummpt2d  33142  gsumpart  33156  symgcom  33176  tocycval  33201  tocycfv  33202  tocycf  33210  tocyc01  33211  cycpm2tr  33212  cycpmconjslem1  33247  cycpmconjslem2  33248  nsgqusf1o  33508  extvval  33707  extvfval  33708  extvfvcl  33712  qtophaus  34013  esumcvg  34263  eulerpartlemn  34558  sseqp1  34572  signsvtn0  34747  ftc2re  34775  reprsuc  34792  bnj1385  35007  bnj1326  35201  bnj1321  35202  bnj1442  35224  bnj1450  35225  bnj1463  35230  bnj1529  35245  f1resfz0f1d  35327  pfxwlk  35337  pthhashvtx  35341  cvmliftlem5  35502  cvmliftlem7  35504  cvmliftlem10  35507  cvmliftlem11  35508  cvmliftlem15  35511  cvmlift2lem11  35526  cvmlift2lem12  35527  satffunlem1lem1  35615  satffunlem2lem1  35617  eldm3  35974  funsseq  35981  finixpnum  37850  poimirlem3  37868  poimirlem4  37869  poimirlem9  37874  sdclem2  37987  prdsbnd2  38040  isdivrngo  38195  drngoi  38196  elrefsymrels2  38898  eleqvrels2  38921  dibffval  41510  hdmapffval  42196  hdmapfval  42197  eqresfnbd  42598  dvun  42723  eldiophb  43108  diophrw  43110  diophin  43123  tfsconcatrev  43699  ofoafg  43705  resisoeq45d  43770  rclexi  43965  rtrclex  43967  rtrclexi  43971  cnvrcl0  43975  dfrtrcl5  43979  dfrcl2  44024  fvmptiunrelexplb0da  44035  sblpnf  44660  fresin2  45525  limsupresuz  46055  limsupvaluz  46060  limsupvaluz2  46090  supcnvlimsup  46092  climrescn  46100  liminfresuz  46136  cncfuni  46238  dvresntr  46270  dvbdfbdioolem1  46280  itgiccshift  46332  itgperiod  46333  dirkercncflem2  46456  fourierdlem46  46504  fourierdlem48  46506  fourierdlem49  46507  fourierdlem58  46516  fourierdlem72  46530  fourierdlem74  46532  fourierdlem75  46533  fourierdlem81  46539  fourierdlem88  46546  fourierdlem89  46547  fourierdlem90  46548  fourierdlem91  46549  fourierdlem92  46550  fourierdlem103  46561  fourierdlem104  46562  fourierdlem112  46570  fouriersw  46583  voncmpl  46973  funcoressn  47396  funressnmo  47400  f1cof1blem  47428  funfocofob  47432  funressndmafv2rn  47577  f1oresf1orab  47643  upgrimpths  48263  isubgrgrim  48283  stgrfv  48307  gpgov  48396  rngcidALTV  48628  rhmsubcALTVlem3  48637  funcringcsetcALTV2lem5  48648  ringcidALTV  48662  funcringcsetclem5ALTV  48671  itcoval  49015  itcoval0mpt  49020  itcovalendof  49023  idfu1sta  49454  idfu2nda  49456  imaidfu2  49464  idfullsubc  49514  dfswapf2  49614  oppc1stf  49641  oppc2ndf  49642  1stfpropd  49643  2ndfpropd  49644  fucofvalg  49671  fucof1  49675  fucofvalne  49678  opf2fval  49758  idfudiag1  49878  aacllem  50154