Theorem reseq2 3361

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 3195	. . 3 |- (A = B -> (A X. V) = (B X. V))
2	1	ineq2d 2213	. 2 |- (A = B -> (C i^i (A X. V)) = (C i^i (B X. V)))
3		df-res 3185	. 2 |- (C |` A) = (C i^i (A X. V))
4		df-res 3185	. 2 |- (C |` B) = (C i^i (B X. V))
5	2, 3, 4	3eqtr4g 1528	1 |- (A = B -> (C |` A) = (C |` B))

Syntax hints:   -> wi 3   = wceq 954  Vcvv 1807   i^i cin 2042   X. cxp 3163   |` cres 3167

This theorem is referenced by:  rescom 3376  resabs1 3380  imaeq2 3394  resdm2 3488  funcnvres 3560  cnvresid 3561  f1orescnv 3695  f1ococnv2 3699  fnressn 3828  fressnfv 3829  tfrlem11 3912  tfr2 3916  tz7.44-1 3919  tz7.44-2 3920  tz7.44-3 3921  rdglem1 3928  oprssoprval 4025  curry1 4088  sbthlem4 4436  seqzfval 6477  seqzfval2 6478  seq1seqz 6481  seq0seqz 6482  facnnt 6878  fac0 6879  sumeq2 6931  climuz0 7053  geolim1i 7181  dfef2 7257  idcn 7716  metres 7775  metcnss 7850  metcnss2 7851  metidcn 7852  isps 8588  dflog2 8691  eff1o2 8693  dfrelog 8695  hhssablt 9072  hhssnvt 9074  hhsssh 9078  ghomgrplem 10323  ghomgrp 10324

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-opab 2662  df-xp 3179  df-res 3185

Copyright terms: Public domain