Theorem reseq1i 4888

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 4886	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1349   ↾ cres 4614

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 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-v 2733  df-in 3128  df-res 4624

This theorem is referenced by:  reseq12i  4890  resindm  4934  resmpt  4940  resmpt3  4941  resmptf  4942  opabresid  4945  rescnvcnv  5075  coires1  5130  fcoi1  5380  fvsnun1  5697  fvsnun2  5698  resoprab  5953  resmpo  5955  ofmres  6119  f1stres  6142  f2ndres  6143  df1st2  6202  df2nd2  6203  dftpos2  6244  tfr2a  6304  freccllem  6385  frecfcllem  6387  frecsuclem  6389  djuf1olemr  7035  divfnzn  9584  cnmptid  13160  xmsxmet2  13342  msmet2  13343