Theorem reseq2 3369

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 3200	. . 3 |- (A = B -> (A X. V) = (B X. V))
2	1	ineq2d 2217	. 2 |- (A = B -> (C i^i (A X. V)) = (C i^i (B X. V)))
3		df-res 3190	. 2 |- (C |` A) = (C i^i (A X. V))
4		df-res 3190	. 2 |- (C |` B) = (C i^i (B X. V))
5	2, 3, 4	3eqtr4g 1531	1 |- (A = B -> (C |` A) = (C |` B))

Syntax hints:   -> wi 3   = wceq 956  Vcvv 1811   i^i cin 2046   X. cxp 3168   |` cres 3172

This theorem is referenced by:  rescom 3384  resabs1 3388  imaeq2 3402  resdm2 3496  funcnvres 3568  cnvresid 3569  f1orescnv 3704  f1ococnv2 3708  fnressn 3837  fressnfv 3838  tfrlem11 3921  tfr2 3925  tz7.44-1 3928  tz7.44-2 3929  tz7.44-3 3930  rdglem1 3937  oprssoprval 4034  curry1 4098  sbthlem4 4448  seqzfval 6523  seqzfval2 6524  seq1seqz 6527  seq0seqz 6528  facnnt 6918  fac0 6919  sumeq2 6970  climuz0 7093  geolim1i 7223  dfef2 7292  idcn 7751  metres 7808  metcnss 7883  metcnss2 7884  metidcn 7885  isps 8630  dflog2 8737  eff1o2 8739  dfrelog 8741  hhssablt 9118  hhssnvt 9120  hhsssh 9124  ghomgrplem 10374  ghomgrp 10375

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-opab 2667  df-xp 3184  df-res 3190

Copyright terms: Public domain