Theorem reseq1i 4823

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

Hypothesis

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
reseq1i	⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 ⊢ 𝐴 = 𝐵
2		reseq1 4821	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1332   ↾ cres 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3082  df-res 4559

This theorem is referenced by:  reseq12i  4825  resindm  4869  resmpt  4875  resmpt3  4876  resmptf  4877  opabresid  4880  rescnvcnv  5009  coires1  5064  fcoi1  5311  fvsnun1  5625  fvsnun2  5626  resoprab  5875  resmpo  5877  ofmres  6042  f1stres  6065  f2ndres  6066  df1st2  6124  df2nd2  6125  dftpos2  6166  tfr2a  6226  freccllem  6307  frecfcllem  6309  frecsuclem  6311  djuf1olemr  6947  divfnzn  9440  cnmptid  12489  xmsxmet2  12671  msmet2  12672