Theorem reseq1i 5033

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

Syntax hints:   = wceq 1398   ↾ cres 4750

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-in 3216  df-res 4760

This theorem is referenced by:  reseq12i  5035  resindm  5079  resmpt  5085  resmpt3  5086  resmptf  5087  opabresid  5090  rescnvcnv  5224  coires1  5279  fresaunres1disj  5545  fcoi1  5546  fvsnun1  5880  fvsnun2  5881  resoprab  6148  resmpo  6150  ofmres  6328  f1stres  6352  f2ndres  6353  df1st2  6414  df2nd2  6415  dftpos2  6491  tfr2a  6551  freccllem  6632  frecfcllem  6634  frecsuclem  6636  djuf1olemr  7344  divfnzn  9952  cnmptid  15138  xmsxmet2  15320  msmet2  15321  cnfldms  15393