Theorem reseq2d 5979

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

Syntax hints:   → wi 4   = wceq 1534   ↾ cres 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-in 3952  df-opab 5205  df-xp 5678  df-res 5684

This theorem is referenced by:  reseq12d  5980  resresdm  6231  relresfld  6274  fnunres1  6660  f1orescnv  6848  fococnv2  6859  fvn0ssdmfun  7078  fnressn  7161  fnsnsplit  7187  oprssov  7584  curry1  8103  curry2  8106  dftpos2  8242  frecseq123  8281  fpr3g  8284  frrlem1  8285  frrlem4  8288  frrlem12  8296  fpr2a  8301  wrecseq123OLD  8314  wfr3g  8321  wfrlem1OLD  8322  wfrlem4OLD  8326  wfrlem14OLD  8336  wfr2aOLD  8340  dfrecs3  8386  dfrecs3OLD  8387  tfrlem16  8407  tfr2ALT  8415  tfr3ALT  8416  on2recsov  8682  sbthlem4  9104  mapunen  9164  hartogslem1  9559  frr3g  9773  frr2  9777  axdc3lem2  10468  fseq1p1m1  13601  resunimafz0  14430  hashf1lem1  14441  hashf1lem1OLD  14442  relexp0g  14995  relexp0  14996  relexpsucnnr  14998  dfrtrcl2  15035  bpolylem  16018  setsval  17129  idfuval  17855  idfu2nd  17856  resf1st  17873  idfusubc0  17878  idfusubc  17879  setcid  18068  catcisolem  18092  estrcid  18117  funcestrcsetclem5  18128  funcsetcestrclem5  18143  funcsetcestrclem7  18145  1stfval  18175  1stf2  18177  2ndfval  18178  2ndf2  18180  1stfcl  18181  2ndfcl  18182  curf2ndf  18232  hofcl  18244  isps  18553  cnvps  18563  isdir  18583  dirref  18586  tsrdir  18589  frmdval  18796  frmdplusg  18799  gsum2dlem2  19919  dprd2da  19992  dpjval  20006  ablfac1eulem  20022  ablfac1eu  20023  rngcval  20544  rnghmsubcsetclem1  20557  rngccat  20560  rngcid  20561  rngcifuestrc  20565  funcrngcsetc  20566  funcrngcsetcALT  20567  ringcval  20573  rhmsubcsetclem1  20586  ringccat  20589  ringcid  20590  rhmsubcrngclem1  20592  rhmsubcrngc  20594  funcringcsetc  20600  rhmsubc  20615  psrplusg  21874  opsrtoslem2  21993  mdetunilem3  22509  mdetunilem4  22510  mdetunilem9  22515  imacmp  23294  ptuncnv  23704  tgphaus  24014  tsmsres  24041  tsmsxplem1  24050  tsmsxplem2  24051  trust  24127  metreslem  24261  imasdsf1olem  24272  xmspropd  24372  mspropd  24373  imasf1oxms  24391  imasf1oms  24392  nmpropd2  24497  isngp2  24499  ngppropd  24539  tngngp2  24562  cphsscph  25172  cmspropd  25270  cmssmscld  25271  mbfres2  25567  limciun  25816  dvmptres3  25881  dvmptres2  25887  dvmptntr  25896  dvlipcn  25920  dvlip2  25921  c1liplem1  25922  dvgt0lem1  25928  lhop1lem  25939  dvcnvrelem1  25943  dvcvx  25946  ftc2ditglem  25973  wilthlem2  26994  dchrval  27160  dchrelbas2  27163  noresle  27623  nosupcbv  27628  nosupno  27629  nosupdm  27630  nosupfv  27632  nosupres  27633  nosupbnd1lem1  27634  nosupbnd1lem3  27636  nosupbnd1lem5  27638  nosupbnd1  27640  nosupbnd2  27642  noinfcbv  27643  noinfno  27644  noinfdm  27645  noinffv  27647  noinfres  27648  noinfbnd1lem3  27651  noinfbnd1lem5  27653  noinfbnd1  27655  noinfbnd2  27657  noetalem1  27667  norecov  27857  norec2ov  27867  egrsubgr  29083  pthdlem1  29573  eupthvdres  30038  eupth2lem3  30039  eupth2  30042  eucrct2eupth  30048  hhssablo  31066  hhssnvt  31068  hhsssh  31072  fressupp  32462  resf1o  32506  gsummpt2d  32757  gsumpart  32763  symgcom  32800  tocycval  32823  tocycfv  32824  tocycf  32832  tocyc01  32833  cycpm2tr  32834  cycpmconjslem1  32869  cycpmconjslem2  32870  nsgqusf1o  33120  qtophaus  33431  esumcvg  33699  eulerpartlemn  33995  sseqp1  34009  signsvtn0  34196  ftc2re  34224  reprsuc  34241  bnj1385  34457  bnj1326  34651  bnj1321  34652  bnj1442  34674  bnj1450  34675  bnj1463  34680  bnj1529  34695  f1resfz0f1d  34717  pfxwlk  34727  pthhashvtx  34731  cvmliftlem5  34893  cvmliftlem7  34895  cvmliftlem10  34898  cvmliftlem11  34899  cvmliftlem15  34902  cvmlift2lem11  34917  cvmlift2lem12  34918  satffunlem1lem1  35006  satffunlem2lem1  35008  eldm3  35349  funsseq  35357  finixpnum  37072  poimirlem3  37090  poimirlem4  37091  poimirlem9  37096  sdclem2  37209  prdsbnd2  37262  isdivrngo  37417  drngoi  37418  elrefsymrels2  38035  eleqvrels2  38058  dibffval  40607  hdmapffval  41293  hdmapfval  41294  eqresfnbd  41717  eldiophb  42171  diophrw  42173  diophin  42186  tfsconcatrev  42771  ofoafg  42777  resisoeq45d  42844  rclexi  43039  rtrclex  43041  rtrclexi  43045  cnvrcl0  43049  dfrtrcl5  43053  dfrcl2  43098  fvmptiunrelexplb0da  43109  sblpnf  43741  fresin2  44539  limsupresuz  45085  limsupvaluz  45090  limsupvaluz2  45120  supcnvlimsup  45122  climrescn  45130  liminfresuz  45166  cncfuni  45268  dvresntr  45300  dvbdfbdioolem1  45310  itgiccshift  45362  itgperiod  45363  dirkercncflem2  45486  fourierdlem46  45534  fourierdlem48  45536  fourierdlem49  45537  fourierdlem58  45546  fourierdlem72  45560  fourierdlem74  45562  fourierdlem75  45563  fourierdlem81  45569  fourierdlem88  45576  fourierdlem89  45577  fourierdlem90  45578  fourierdlem91  45579  fourierdlem92  45580  fourierdlem103  45591  fourierdlem104  45592  fourierdlem112  45600  fouriersw  45613  voncmpl  46003  funcoressn  46418  funressnmo  46422  f1cof1blem  46450  funfocofob  46452  funressndmafv2rn  46597  f1oresf1orab  46663  rngcidALTV  47330  rhmsubcALTVlem3  47339  funcringcsetcALTV2lem5  47350  ringcidALTV  47364  funcringcsetclem5ALTV  47373  itcoval  47728  itcoval0mpt  47733  itcovalendof  47736  aacllem  48228

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »