Theorem reseq2 3353

Description: Equality theorem for restrictions.

Assertion

Ref	Expression
reseq2	|- (A = B -> (C |` A) = (C |` B))

Proof of Theorem reseq2

Step	Hyp	Ref	Expression
1		xpeq1 3190	. . 3 |- (A = B -> (A X. V) = (B X. V))
2	1	ineq2d 2207	. 2 |- (A = B -> (C i^i (A X. V)) = (C i^i (B X. V)))
3		df-res 3180	. 2 |- (C |` A) = (C i^i (A X. V))
4		df-res 3180	. 2 |- (C |` B) = (C i^i (B X. V))
5	2, 3, 4	3eqtr4g 1523	1 |- (A = B -> (C |` A) = (C |` B))

Syntax hints:   -> wi 3   = wceq 953  Vcvv 1802   i^i cin 2036   X. cxp 3158   |` cres 3162

This theorem is referenced by:  rescom 3368  resabs1 3372  imaeq2 3386  resdm2 3482  funcnvres 3554  cnvresid 3555  f1orescnv 3689  f1ococnv2 3693  fnressn 3822  fressnfv 3823  tfrlem11 3906  tfr2 3910  tz7.44-1 3913  tz7.44-2 3914  tz7.44-3 3915  rdglem1 3922  oprssoprval 4019  curry1 4082  sbthlem4 4430  seqzfval 6469  seqzfval2 6470  seq1seqz 6473  seq0seqz 6474  facnnt 6870  fac0 6871  sumeq2 6923  climuz0 7045  geolim1i 7173  dfef2 7249  idcn 7705  metres 7763  metcnss 7837  metcnss2 7838  metidcn 7839  isps 8571  dflog2 8674  eff1o2 8676  dfrelog 8678  hhssnvt 9055  hhsssh 9059  ghomgrplem 10294  ghomgrp 10295

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-in 2041  df-opab 2657  df-xp 3174  df-res 3180

Copyright terms: Public domain