Theorem reseq2 4895

Description: Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)

Assertion

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

Proof of Theorem reseq2

Step	Hyp	Ref	Expression
1		xpeq1 4634	. . 3 |- ( A = B -> ( A X. _V ) = ( B X. _V ) )
2	1	ineq2d 3334	. 2 |- ( A = B -> ( C i^i ( A X. _V ) ) = ( C i^i ( B X. _V ) ) )
3		df-res 4632	. 2 |- ( C |` A ) = ( C i^i ( A X. _V ) )
4		df-res 4632	. 2 |- ( C |` B ) = ( C i^i ( B X. _V ) )
5	2, 3, 4	3eqtr4g 2233	1 |- ( A = B -> ( C |` A ) = ( C |` B ) )

Syntax hints:   -> wi 4   = wceq 1353   _Vcvv 2735   i^i cin 3126   X. cxp 4618   |` cres 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-in 3133  df-opab 4060  df-xp 4626  df-res 4632

This theorem is referenced by:  reseq2i  4897  reseq2d  4900  resabs1  4929  resima2  4934  imaeq2  4959  resdisj  5049  relcoi1  5152  fressnfv  5695  tfrlem1  6299  tfrlem9  6310  tfr0dm  6313  tfrlemisucaccv  6316  tfrlemiubacc  6321  tfr1onlemsucaccv  6332  tfr1onlemubacc  6337  tfr1onlemaccex  6339  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllemubacc  6350  tfrcllemaccex  6352  tfrcllemres  6353  tfrcldm  6354  fnfi  6926  lmbr2  13283  lmff  13318