Theorem reseq2d 5983

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↾ cres 5668

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-in 3915  df-opab 5179  df-xp 5672  df-res 5678

This theorem is used by:  reseq12d  5984  imadifssranOLD  6208  resresdm  6239  relresfld  6283  relresfldOLD  6284  fnunres1  6654  f1orescnv  6843  fococnv2  6854  fvn0ssdmfun  7076  fnressn  7162  fnsnsplit  7189  oprssov  7592  curry1  8108  curry2  8111  dftpos2  8248  frecseq123  8288  fpr3g  8291  frrlem1  8292  frrlem4  8295  frrlem12  8303  fpr2a  8308  wfr3g  8325  dfrecs3  8368  tfrlem16  8389  tfr2ALT  8397  tfr3ALT  8398  on2recsov  8663  sbthlem4  9088  mapunen  9144  hartogslem1  9514  frr3g  9738  frr2  9742  axdc3lem2  10453  fseq1p1m1  13645  f1resfz0f1d  13840  resunimafz0  14502  hashf1lem1  14512  relexp0g  15085  relexp0  15086  relexpsucnnr  15088  dfrtrcl2  15125  bpolylem  16127  setsval  17252  idfuval  17958  idfu2nd  17959  resf1st  17976  idfusubc0  17981  idfusubc  17982  setcid  18168  catcisolem  18192  estrcid  18215  funcestrcsetclem5  18225  funcsetcestrclem5  18240  funcsetcestrclem7  18242  1stfval  18272  1stf2  18274  2ndfval  18275  2ndf2  18277  1stfcl  18278  2ndfcl  18279  curf2ndf  18328  hofcl  18340  isps  18649  cnvps  18659  isdir  18679  dirref  18682  tsrdir  18685  frmdval  18941  frmdplusg  18944  gsum2dlem2  20072  dprd2da  20145  dpjval  20159  ablfac1eulem  20175  ablfac1eu  20176  rngcval  20754  rnghmsubcsetclem1  20767  rngccat  20770  rngcid  20771  rngcifuestrc  20775  funcrngcsetc  20776  funcrngcsetcALT  20777  ringcval  20783  rhmsubcsetclem1  20796  ringccat  20799  ringcid  20800  rhmsubcrngclem1  20802  rhmsubcrngc  20804  funcringcsetc  20810  rhmsubc  20825  psrplusg  22124  opsrtoslem2  22244  mdetunilem3  22808  mdetunilem4  22809  mdetunilem9  22814  imacmp  23591  ptuncnv  24001  tgphaus  24311  tsmsres  24338  tsmsxplem1  24347  tsmsxplem2  24348  trust  24423  metreslem  24556  imasdsf1olem  24567  xmspropd  24667  mspropd  24668  imasf1oxms  24683  imasf1oms  24684  nmpropd2  24789  isngp2  24791  ngppropd  24831  tngngp2  24846  cphsscph  25447  cmspropd  25545  cmssmscld  25546  mbfres2  25841  limciun  26090  dvmptres3  26152  dvmptres2  26158  dvmptntr  26167  dvlipcn  26190  dvlip2  26191  c1liplem1  26192  dvgt0lem1  26198  lhop1lem  26209  dvcnvrelem1  26213  dvcvx  26216  ftc2ditglem  26241  wilthlem2  27270  dchrval  27435  dchrelbas2  27438  noresle  27898  nosupcbv  27903  nosupno  27904  nosupdm  27905  nosupfv  27907  nosupres  27908  nosupbnd1lem1  27909  nosupbnd1lem3  27911  nosupbnd1lem5  27913  nosupbnd1  27915  nosupbnd2  27917  noinfcbv  27918  noinfno  27919  noinfdm  27920  noinffv  27922  noinfres  27923  noinfbnd1lem3  27926  noinfbnd1lem5  27928  noinfbnd1  27930  noinfbnd2  27932  noetalem1  27942  norecov  28177  norec2ov  28187  egrsubgr  29664  dfpth2  30115  pthdlem1  30152  eupthvdres  30623  eupth2lem3  30624  eupth2  30627  eucrct2eupth  30633  hhssablo  31652  hhssnvt  31654  hhsssh  31658  fresunsn  33007  fressupp  33070  resf1o  33112  gsummpt2d  33400  gsumpart  33414  symgcom  33434  tocycval  33459  tocycfv  33460  tocycf  33468  tocyc01  33469  cycpm2tr  33470  cycpmconjslem1  33505  cycpmconjslem2  33506  nsgqusf1o  33756  extvval  33952  extvfval  33953  extvfvcl  33957  qtophaus  34257  esumcvg  34507  eulerpartlemn  34802  sseqp1  34816  signsvtn0  34988  ftc2re  35016  reprsuc  35033  bnj1385  35251  bnj1326  35445  bnj1321  35446  bnj1442  35468  bnj1450  35469  bnj1463  35474  bnj1529  35489  pfxwlk  35636  pthhashvtx  35640  cvmliftlem5  35801  cvmliftlem7  35803  cvmliftlem10  35806  cvmliftlem11  35807  cvmliftlem15  35810  cvmlift2lem11  35825  cvmlift2lem12  35826  satffunlem1lem1  35914  satffunlem2lem1  35916  eldm3  36273  funsseq  36280  finixpnum  38296  poimirlem3  38314  poimirlem4  38315  poimirlem9  38320  sdclem2  38433  prdsbnd2  38486  isdivrngo  38641  drngoi  38642  elrefsymrels2  39342  eleqvrels2  39365  dibffval  41954  hdmapffval  42640  hdmapfval  42641  eqresfnbd  43043  dvun  43160  eldiophb  43528  diophrw  43530  diophin  43543  tfsconcatrev  44115  ofoafg  44121  resisoeq45d  44186  rclexi  44381  rtrclex  44383  rtrclexi  44387  cnvrcl0  44391  dfrtrcl5  44395  dfrcl2  44440  fvmptiunrelexplb0da  44451  sblpnf  45060  fresin2  45930  limsupresuz  46457  limsupvaluz  46462  limsupvaluz2  46492  supcnvlimsup  46494  climrescn  46502  liminfresuz  46538  cncfuni  46640  dvresntr  46672  dvbdfbdioolem1  46682  itgiccshift  46734  itgperiod  46735  dirkercncflem2  46858  fourierdlem46  46906  fourierdlem48  46908  fourierdlem49  46909  fourierdlem58  46918  fourierdlem72  46932  fourierdlem74  46934  fourierdlem75  46935  fourierdlem81  46941  fourierdlem88  46948  fourierdlem89  46949  fourierdlem90  46950  fourierdlem91  46951  fourierdlem92  46952  fourierdlem103  46963  fourierdlem104  46964  fourierdlem112  46972  fouriersw  46985  voncmpl  47375  funcoressn  47819  funressnmo  47823  f1cof1blem  47851  funfocofob  47855  funressndmafv2rn  48000  f1oresf1orab  48066  upgrimpths  48714  isubgrgrim  48734  stgrfv  48758  gpgov  48847  rngcidALTV  49079  rhmsubcALTVlem3  49088  funcringcsetcALTV2lem5  49099  ringcidALTV  49113  funcringcsetclem5ALTV  49122  itcoval  49481  itcoval0mpt  49486  itcovalendof  49489  idfu1sta  49919  idfu2nda  49921  imaidfu2  49929  idfullsubc  49979  dfswapf2  50079  oppc1stf  50106  oppc2ndf  50107  1stfpropd  50108  2ndfpropd  50109  fucofvalg  50136  fucof1  50140  fucofvalne  50143  opf2fval  50223  idfudiag1  50343  aacllem  50661