Theorem reseq2d 4943

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3160  df-opab 4092  df-xp 4666  df-res 4672

This theorem is referenced by:  reseq12d  4944  resima2  4977  relresfld  5196  f1orescnv  5517  funcocnv2  5526  fococnv2  5527  fnressn  5745  oprssov  6062  dftpos2  6316  fnsnsplitdc  6560  dif1en  6937  sbthlemi4  7021  fseq1p1m1  10163  resunimafz0  10905  setsvala  12652  metreslem  14559  xmspropd  14656  mspropd  14657  bj-charfundcALT  15371