Theorem reseq1i 4741

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

Hypothesis

Ref	Expression
reseqi.1	|- A = B

Assertion

Ref	Expression
reseq1i	|- ( A |` C ) = ( B |` C )

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 |- A = B
2		reseq1 4739	. 2 |- ( A = B -> ( A |` C ) = ( B |` C ) )
3	1, 2	ax-mp 7	1 |- ( A |` C ) = ( B |` C )

Syntax hints:   = wceq 1296   |` cres 4469

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-in 3019  df-res 4479

This theorem is referenced by:  reseq12i  4743  resindm  4787  resmpt  4793  resmpt3  4794  resmptf  4795  opabresid  4798  rescnvcnv  4927  coires1  4982  fcoi1  5226  fvsnun1  5533  fvsnun2  5534  resoprab  5779  resmpt2  5781  ofmres  5945  f1stres  5968  f2ndres  5969  df1st2  6022  df2nd2  6023  dftpos2  6064  tfr2a  6124  freccllem  6205  frecfcllem  6207  frecsuclem  6209  djuf1olemr  6826  divfnzn  9205  cnmptid  12119  xmsxmet2  12265  msmet2  12266