Theorem reseq2i 5973

Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵

Assertion

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

Proof of Theorem reseq2i

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

Syntax hints:   = wceq 1567   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920  df-opab 5175  df-xp 5665  df-res 5671

This theorem is referenced by:  reseq12i  5974  rescom  5999  resindm  6027  resdmdfsn  6029  resdmdfsnOLD  6030  idinxpresid  6048  rescnvcnv  6202  resdm2  6229  funcnvres  6611  resasplit  6746  fresaunres2  6748  fresaunres1  6749  resdif  6840  resin  6841  funcocnv2  6844  fvn0ssdmfun  7067  residpr  7137  eqfunressuc  7357  fprlem1  8293  domss2  9120  ordtypelem1  9476  frrlem15  9725  ackbij2lem3  10219  facnn  14307  fac0  14308  hashresfn  14372  relexpcnv  15068  divcnvshft  15905  ruclem4  16286  fsets  17225  setsid  17263  join0  18455  meet0  18456  symgfixelsi  19501  psgnsn  19586  dprd2da  20110  ply1plusgfvi  22366  uptx  23747  txcn  23748  ressxms  24647  ressms  24648  iscmet3lem3  25414  volres  25652  dvlip  26117  dvne0  26135  lhop  26140  dflog2  26687  dfrelog  26692  dvlog  26778  wilthlem2  27195  nosupbnd2lem1  27841  noinfbnd2lem1  27856  0grsubgr  29565  0pth  30413  1pthdlem1  30423  eupth2lemb  30525  ex-fpar  30750  fressupp  32970  df1stres  32986  df2ndres  32987  ffsrn  33010  resf1o  33012  fpwrelmapffs  33016  cycpmconjv  33399  evlextv  33873  sitmcl  34682  eulerpartlemn  34712  bnj1326  35355  satfv1lem  35749  divcnvlin  36120  poimirlem9  38163  zrdivrng  38487  isdrngo1  38490  cnvresrn  38882  dfsucmap2  38998  ressucdifsn  39022  disjsuc  39393  eldioph4b  43423  diophren  43425  rclexi  44226  rtrclex  44228  cnvrcl0  44236  dfrtrcl5  44240  dfrcl2  44285  relexpiidm  44315  relexp01min  44324  relexpaddss  44329  seff  44904  sblpnf  44905  radcnvrat  44909  hashnzfzclim  44917  dvresioo  46520  fourierdlem72  46777  fourierdlem80  46785  fourierdlem94  46799  fourierdlem103  46808  fourierdlem104  46809  fourierdlem113  46818  fouriersw  46830  sge0split  47008  isubgrgrim  48576  stgr0  48607  stgr1  48608  rngcidALTV  48921  ringcidALTV  48955  tposresg  49534  tposres3  49537  tposresxp  49539