Theorem reseq1i 5009

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 5007	. 2 |- ( A = B -> ( A |` C ) = ( B |` C ) )
3	1, 2	ax-mp 5	1 |- ( A |` C ) = ( B |` C )

Syntax hints:   = wceq 1397   |` cres 4727

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206  df-res 4737

This theorem is referenced by:  reseq12i  5011  resindm  5055  resmpt  5061  resmpt3  5062  resmptf  5063  opabresid  5066  rescnvcnv  5199  coires1  5254  fcoi1  5517  fvsnun1  5850  fvsnun2  5851  resoprab  6116  resmpo  6118  ofmres  6297  f1stres  6321  f2ndres  6322  df1st2  6383  df2nd2  6384  dftpos2  6426  tfr2a  6486  freccllem  6567  frecfcllem  6569  frecsuclem  6571  djuf1olemr  7252  divfnzn  9854  cnmptid  15004  xmsxmet2  15186  msmet2  15187  cnfldms  15259