Theorem reseq2d 5115

Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
reseq2d	|- ( ph -> ( C |` A ) = ( C |` B ) )

Proof of Theorem reseq2d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 |- ( ph -> A = B )
2		reseq2 5110	. 2 |- ( A = B -> ( C |` A ) = ( C |` B ) )
3	1, 2	syl 16	1 |- ( ph -> ( C |` A ) = ( C |` B ) )

Syntax hints:   -> wi 4   = wceq 1369   |` cres 4847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340  df-opab 4356  df-xp 4851  df-res 4857

This theorem is referenced by:  reseq12d  5116  resima2  5148  resdmdfsn  5157  relresfld  5369  f1orescnv  5661  funcocnv2  5670  fococnv2  5671  fnressn  5899  fnsnsplit  5920  oprssov  6237  curry1  6669  curry2  6672  dftpos2  6767  tfrlem16  6857  sbthlem4  7429  mapunen  7485  hartogslem1  7761  axdc3lem2  8625  fseq1p1m1  11539  hashf1lem1  12213  setsval  14203  idfuval  14791  idfu2nd  14792  resf1st  14809  setcid  14959  catcisolem  14979  1stfval  15006  1stf2  15008  2ndfval  15009  2ndf2  15011  1stfcl  15012  2ndfcl  15013  curf2ndf  15062  hofcl  15074  isps  15377  cnvps  15387  isdir  15407  dirref  15410  tsrdir  15413  frmdval  15534  frmdplusg  15537  gsum2dlem2  16467  gsum2dOLD  16469  dprd2da  16546  dpjval  16560  ablfac1eulem  16578  ablfac1eu  16579  psrplusg  17457  opsrtoslem2  17571  mdetunilem3  18425  mdetunilem4  18426  mdetunilem9  18431  imacmp  19005  ptuncnv  19385  tgphaus  19692  tsmsresOLD  19722  tsmsres  19723  tsmsxplem1  19732  tsmsxplem2  19733  trust  19809  metreslem  19942  imasdsf1olem  19953  xmspropd  20053  mspropd  20054  imasf1oxms  20069  imasf1oms  20070  nmpropd2  20192  isngp2  20194  ngppropd  20228  tngngp2  20243  cmspropd  20865  mbfres2  21128  limciun  21374  dvmptres3  21435  dvmptres2  21441  dvmptntr  21450  dvlipcn  21471  dvlip2  21472  c1liplem1  21473  dvgt0lem1  21479  lhop1lem  21490  dvcnvrelem1  21494  dvcvx  21497  ftc2ditglem  21522  wilthlem2  22412  dchrval  22578  dchrelbas2  22581  1pthonlem1  23493  constr2pth  23505  eupath2lem3  23605  eupath2  23606  efghgrp  23865  drngoi  23899  isdivrngo  23923  hhssablo  24669  hhssnvt  24671  hhsssh  24675  resf1o  26035  esumcvg  26540  eulerpartlemn  26769  sseqp1  26783  signsvtn0  26976  cvmliftlem5  27183  cvmliftlem7  27185  cvmliftlem10  27188  cvmliftlem11  27189  cvmliftlem15  27192  cvmlift2lem11  27207  cvmlift2lem12  27208  ghomgrplem  27313  relexp0  27336  relexpsucr  27337  dfrtrcl2  27355  eldm3  27577  funsseq  27585  wrecseq123  27723  wfr3g  27728  wfrlem1  27729  wfrlem4  27732  wfrlem14  27742  wfr2  27746  tfrALTlem  27748  tfr2ALT  27750  tfr3ALT  27751  frr3g  27772  frrlem1  27773  frrlem4  27776  bpolylem  28196  finixpnum  28419  sdclem2  28643  prdsbnd2  28699  eldiophb  29100  diophrw  29102  diophin  29116  sblpnf  29601  funcoressn  30038  usgra2pthspth  30300  bnj1385  31831  bnj1326  32022  bnj1321  32023  bnj1442  32045  bnj1450  32046  bnj1463  32051  bnj1529  32066  dibffval  34790  hdmapffval  35479  hdmapfval  35480