Theorem reseq1i 5972

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

This proof depends on syntax axioms:   = wceq 1570   ↾ cres 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3909  df-res 5671

This theorem is used by:  reseq12i  5974  resindmOLD  6028  resmpt  6037  resmpt3  6038  resmptf  6039  elimampt  6043  opabresid  6050  rescnvcnv  6204  coires1  6265  fnunres2  6649  fresaunres1  6752  fcoi1  6753  fninfp  7176  fvsnun1  7184  fvsnun2  7185  resoprab  7535  resmpo  7537  elimampo  7554  elrnmpores  7555  ofmres  7985  f1stres  8014  f2ndres  8015  df1st2  8099  df2nd2  8100  fsplitfpar  8119  dftpos2  8245  frrlem12  8300  tfr2a  8388  tfr2b  8389  rdgseg  8415  frsucmpt2  8433  seqomlem2  8444  seqomlem3  8445  seqomlem4  8446  domss2  9138  dffi3  9405  axdc  10527  fpwwe2lem12  10655  seqval  14080  hashgval  14401  hashinf  14403  submefmnd  19010  pgrpsubgsymg  19542  gsumzunsnd  20089  ablfac1b  20205  zzngim  21771  pmatcollpw3lem  23014  txflf  24238  xmsxmet2  24691  msmet2  24692  tmsxpsmopn  24769  isngp2  24829  subgnm  24865  tngngp2  24884  cnfldms  25007  msdcn  25074  oprpiece1res1  25185  oprpiece1res2  25186  isncvsngp  25383  cncms  25589  cnfldcusp  25591  reust  25615  minveclem3a  25661  dvreslem  26143  dvres2lem  26144  dvmptresicc  26150  dvcmulf  26179  mdegfval  26294  psercn  26669  abelth  26684  efcvx  26692  efifo  26792  dfrelog  26810  dvrelog  26882  dvlog  26896  efopnlem2  26902  dvatan  27180  dchrisumlem1  27733  noetasuplem2  27978  noetasuplem3  27979  noetasuplem4  27980  noetainflem2  27982  wlknwwlksnbij  30364  df1stres  33184  df2ndres  33185  padct  33197  ressplusf  33411  ressnm  33412  gsummpt2d  33497  cycpmrn  33591  tocyccntz  33592  cycpmconjslem2  33603  qusima  33845  qqhcn  34509  cnrrext  34528  rrhre  34539  esumcvg  34604  dya2icoseg2  34797  eulerpartgbij  34891  satf0  35959  neibastop2  36988  mptsnunlem  38100  icorempo  38113  poimirlem3  38380  mbfposadd  38424  ftc1anclem3  38452  dvasin  38461  dvacos  38462  prdsbnd2  38553  repwsmet  38592  rrnequiv  38593  inres2  39003  xrnres  39181  xrnres2  39182  xrnres3  39183  diophin  43625  eldioph4b  43660  dnnumch1  43893  aomclem6  43908  radcnvrat  45146  lhe4.4ex1a  45161  dvsid  45163  dvsef  45164  imassmpt  46099  elicores  46371  climresmpt  46495  dvcosre  46748  itgsinexplem1  46790  fourierdlem40  46983  fourierdlem57  46999  fourierdlem58  47000  fourierdlem62  47004  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem80  47022  fourierdlem84  47026  fourierdlem85  47027  fourierdlem101  47043  fourierdlem102  47044  fourierdlem111  47053  fourierdlem114  47056  fouriersw  47067  fouriercn  47068  volicorescl  47389  fdmdifeqresdif  49280  tposresg  49812  tposrescnv  49813  rescofuf  50027  aacllem  50780