Theorem reseq2d 5106

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 5101	. 2 |- ( A = B -> ( C |` A ) = ( C |` B ) )
3	1, 2	syl 16	1 |- ( ph -> ( C |` A ) = ( C |` B ) )

Syntax hints:   -> wi 4   = wceq 1364   |` cres 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332  df-opab 4348  df-xp 4842  df-res 4848

This theorem is referenced by:  reseq12d  5107  resima2  5140  resdmdfsn  5149  relresfld  5361  f1orescnv  5653  funcocnv2  5662  fococnv2  5663  fnressn  5891  fnsnsplit  5912  oprssov  6231  curry1  6663  curry2  6666  dftpos2  6761  tfrlem16  6848  sbthlem4  7420  mapunen  7476  hartogslem1  7752  axdc3lem2  8616  fseq1p1m1  11530  hashf1lem1  12204  setsval  14194  idfuval  14782  idfu2nd  14783  resf1st  14800  setcid  14950  catcisolem  14970  1stfval  14997  1stf2  14999  2ndfval  15000  2ndf2  15002  1stfcl  15003  2ndfcl  15004  curf2ndf  15053  hofcl  15065  isps  15368  cnvps  15378  isdir  15398  dirref  15401  tsrdir  15404  frmdval  15522  frmdplusg  15525  gsum2dlem2  16452  gsum2dOLD  16454  dprd2da  16531  dpjval  16545  ablfac1eulem  16563  ablfac1eu  16564  psrplusg  17430  opsrtoslem2  17542  mdetunilem3  18379  mdetunilem4  18380  mdetunilem9  18385  imacmp  18959  ptuncnv  19339  tgphaus  19646  tsmsresOLD  19676  tsmsres  19677  tsmsxplem1  19686  tsmsxplem2  19687  trust  19763  metreslem  19896  imasdsf1olem  19907  xmspropd  20007  mspropd  20008  imasf1oxms  20023  imasf1oms  20024  nmpropd2  20146  isngp2  20148  ngppropd  20182  tngngp2  20197  cmspropd  20819  mbfres2  21082  limciun  21328  dvmptres3  21389  dvmptres2  21395  dvmptntr  21404  dvlipcn  21425  dvlip2  21426  c1liplem1  21427  dvgt0lem1  21433  lhop1lem  21444  dvcnvrelem1  21448  dvcvx  21451  ftc2ditglem  21476  wilthlem2  22366  dchrval  22532  dchrelbas2  22535  1pthonlem1  23423  constr2pth  23435  eupath2lem3  23535  eupath2  23536  efghgrp  23795  drngoi  23829  isdivrngo  23853  hhssablo  24599  hhssnvt  24601  hhsssh  24605  resf1o  25965  esumcvg  26471  eulerpartlemn  26694  sseqp1  26708  signsvtn0  26901  cvmliftlem5  27108  cvmliftlem7  27110  cvmliftlem10  27113  cvmliftlem11  27114  cvmliftlem15  27117  cvmlift2lem11  27132  cvmlift2lem12  27133  ghomgrplem  27237  relexp0  27260  relexpsucr  27261  dfrtrcl2  27279  eldm3  27501  funsseq  27509  wrecseq123  27647  wfr3g  27652  wfrlem1  27653  wfrlem4  27656  wfrlem14  27666  wfr2  27670  tfrALTlem  27672  tfr2ALT  27674  tfr3ALT  27675  frr3g  27696  frrlem1  27697  frrlem4  27700  bpolylem  28120  finixpnum  28339  sdclem2  28563  prdsbnd2  28619  eldiophb  29020  diophrw  29022  diophin  29036  sblpnf  29521  funcoressn  29958  usgra2pthspth  30220  bnj1385  31660  bnj1326  31851  bnj1321  31852  bnj1442  31874  bnj1450  31875  bnj1463  31880  bnj1529  31895  dibffval  34507  hdmapffval  35196  hdmapfval  35197