Theorem reseq1d 5037

Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

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

Assertion

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

Proof of Theorem reseq1d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 |- ( ph -> A = B )
2		reseq1 5032	. 2 |- ( A = B -> ( A |` C ) = ( B |` C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A |` C ) = ( B |` C ) )

Syntax hints:   -> wi 4   = wceq 1398   |` cres 4751

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217  df-res 4761

This theorem is referenced by:  reseq12d  5039  fun2ssres  5396  funcnvres2  5431  funimaexg  5440  fresin  5543  offres  6328  tfrlemisucaccv  6556  tfrlemi1  6563  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  freceq1  6623  freceq2  6624  fseq1p1m1  10428  setsresg  13250  setscom  13252  znle2  14800  dvcoapbr  15572  bj-charfundcALT  16579