Theorem reseq2d 5938

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 5933	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

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

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 3391  df-in 3897  df-opab 5149  df-xp 5630  df-res 5636

This theorem is referenced by:  reseq12d  5939  imadifssran  6109  resresdm  6191  relresfld  6234  fnunres1  6604  f1orescnv  6789  fococnv2  6800  fvn0ssdmfun  7020  fnressn  7105  fnsnsplit  7132  oprssov  7529  curry1  8047  curry2  8050  dftpos2  8186  frecseq123  8225  fpr3g  8228  frrlem1  8229  frrlem4  8232  frrlem12  8240  fpr2a  8245  wfr3g  8262  dfrecs3  8305  tfrlem16  8325  tfr2ALT  8333  tfr3ALT  8334  on2recsov  8597  sbthlem4  9021  mapunen  9077  hartogslem1  9450  frr3g  9671  frr2  9675  axdc3lem2  10364  fseq1p1m1  13543  resunimafz0  14398  hashf1lem1  14408  relexp0g  14975  relexp0  14976  relexpsucnnr  14978  dfrtrcl2  15015  bpolylem  16004  setsval  17128  idfuval  17834  idfu2nd  17835  resf1st  17852  idfusubc0  17857  idfusubc  17858  setcid  18044  catcisolem  18068  estrcid  18091  funcestrcsetclem5  18101  funcsetcestrclem5  18116  funcsetcestrclem7  18118  1stfval  18148  1stf2  18150  2ndfval  18151  2ndf2  18153  1stfcl  18154  2ndfcl  18155  curf2ndf  18204  hofcl  18216  isps  18525  cnvps  18535  isdir  18555  dirref  18558  tsrdir  18561  frmdval  18810  frmdplusg  18813  gsum2dlem2  19937  dprd2da  20010  dpjval  20024  ablfac1eulem  20040  ablfac1eu  20041  rngcval  20586  rnghmsubcsetclem1  20599  rngccat  20602  rngcid  20603  rngcifuestrc  20607  funcrngcsetc  20608  funcrngcsetcALT  20609  ringcval  20615  rhmsubcsetclem1  20628  ringccat  20631  ringcid  20632  rhmsubcrngclem1  20634  rhmsubcrngc  20636  funcringcsetc  20642  rhmsubc  20657  psrplusg  21926  opsrtoslem2  22044  mdetunilem3  22589  mdetunilem4  22590  mdetunilem9  22595  imacmp  23372  ptuncnv  23782  tgphaus  24092  tsmsres  24119  tsmsxplem1  24128  tsmsxplem2  24129  trust  24204  metreslem  24337  imasdsf1olem  24348  xmspropd  24448  mspropd  24449  imasf1oxms  24464  imasf1oms  24465  nmpropd2  24570  isngp2  24572  ngppropd  24612  tngngp2  24627  cphsscph  25228  cmspropd  25326  cmssmscld  25327  mbfres2  25622  limciun  25871  dvmptres3  25933  dvmptres2  25939  dvmptntr  25948  dvlipcn  25971  dvlip2  25972  c1liplem1  25973  dvgt0lem1  25979  lhop1lem  25990  dvcnvrelem1  25994  dvcvx  25997  ftc2ditglem  26022  wilthlem2  27046  dchrval  27211  dchrelbas2  27214  noresle  27675  nosupcbv  27680  nosupno  27681  nosupdm  27682  nosupfv  27684  nosupres  27685  nosupbnd1lem1  27686  nosupbnd1lem3  27688  nosupbnd1lem5  27690  nosupbnd1  27692  nosupbnd2  27694  noinfcbv  27695  noinfno  27696  noinfdm  27697  noinffv  27699  noinfres  27700  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noinfbnd1  27707  noinfbnd2  27709  noetalem1  27719  norecov  27953  norec2ov  27963  egrsubgr  29360  dfpth2  29812  pthdlem1  29849  eupthvdres  30320  eupth2lem3  30321  eupth2  30324  eucrct2eupth  30330  hhssablo  31349  hhssnvt  31351  hhsssh  31355  fresunsn  32713  fressupp  32776  resf1o  32818  gsummpt2d  33125  gsumpart  33139  symgcom  33159  tocycval  33184  tocycfv  33185  tocycf  33193  tocyc01  33194  cycpm2tr  33195  cycpmconjslem1  33230  cycpmconjslem2  33231  nsgqusf1o  33491  extvval  33690  extvfval  33691  extvfvcl  33695  qtophaus  33996  esumcvg  34246  eulerpartlemn  34541  sseqp1  34555  signsvtn0  34730  ftc2re  34758  reprsuc  34775  bnj1385  34990  bnj1326  35184  bnj1321  35185  bnj1442  35207  bnj1450  35208  bnj1463  35213  bnj1529  35228  f1resfz0f1d  35312  pfxwlk  35322  pthhashvtx  35326  cvmliftlem5  35487  cvmliftlem7  35489  cvmliftlem10  35492  cvmliftlem11  35493  cvmliftlem15  35496  cvmlift2lem11  35511  cvmlift2lem12  35512  satffunlem1lem1  35600  satffunlem2lem1  35602  eldm3  35959  funsseq  35966  finixpnum  37940  poimirlem3  37958  poimirlem4  37959  poimirlem9  37964  sdclem2  38077  prdsbnd2  38130  isdivrngo  38285  drngoi  38286  elrefsymrels2  38988  eleqvrels2  39011  dibffval  41600  hdmapffval  42286  hdmapfval  42287  eqresfnbd  42687  dvun  42805  eldiophb  43203  diophrw  43205  diophin  43218  tfsconcatrev  43794  ofoafg  43800  resisoeq45d  43865  rclexi  44060  rtrclex  44062  rtrclexi  44066  cnvrcl0  44070  dfrtrcl5  44074  dfrcl2  44119  fvmptiunrelexplb0da  44130  sblpnf  44755  fresin2  45620  limsupresuz  46149  limsupvaluz  46154  limsupvaluz2  46184  supcnvlimsup  46186  climrescn  46194  liminfresuz  46230  cncfuni  46332  dvresntr  46364  dvbdfbdioolem1  46374  itgiccshift  46426  itgperiod  46427  dirkercncflem2  46550  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem58  46610  fourierdlem72  46624  fourierdlem74  46626  fourierdlem75  46627  fourierdlem81  46633  fourierdlem88  46640  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem92  46644  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  fouriersw  46677  voncmpl  47067  funcoressn  47502  funressnmo  47506  f1cof1blem  47534  funfocofob  47538  funressndmafv2rn  47683  f1oresf1orab  47749  upgrimpths  48397  isubgrgrim  48417  stgrfv  48441  gpgov  48530  rngcidALTV  48762  rhmsubcALTVlem3  48771  funcringcsetcALTV2lem5  48782  ringcidALTV  48796  funcringcsetclem5ALTV  48805  itcoval  49149  itcoval0mpt  49154  itcovalendof  49157  idfu1sta  49588  idfu2nda  49590  imaidfu2  49598  idfullsubc  49648  dfswapf2  49748  oppc1stf  49775  oppc2ndf  49776  1stfpropd  49777  2ndfpropd  49778  fucofvalg  49805  fucof1  49809  fucofvalne  49812  opf2fval  49892  idfudiag1  50012  aacllem  50288