Theorem reseq1i 4960

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

Syntax hints:   = wceq 1373   ↾ cres 4681

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-in 3173  df-res 4691

This theorem is referenced by:  reseq12i  4962  resindm  5006  resmpt  5012  resmpt3  5013  resmptf  5014  opabresid  5017  rescnvcnv  5150  coires1  5205  fcoi1  5463  fvsnun1  5788  fvsnun2  5789  resoprab  6048  resmpo  6050  ofmres  6228  f1stres  6252  f2ndres  6253  df1st2  6312  df2nd2  6313  dftpos2  6354  tfr2a  6414  freccllem  6495  frecfcllem  6497  frecsuclem  6499  djuf1olemr  7163  divfnzn  9749  cnmptid  14797  xmsxmet2  14979  msmet2  14980  cnfldms  15052