Theorem reseq2 4678

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 4427	. . 3 |- ( A = B -> ( A X. _V ) = ( B X. _V ) )
2	1	ineq2d 3190	. 2 |- ( A = B -> ( C i^i ( A X. _V ) ) = ( C i^i ( B X. _V ) ) )
3		df-res 4425	. 2 |- ( C |` A ) = ( C i^i ( A X. _V ) )
4		df-res 4425	. 2 |- ( C |` B ) = ( C i^i ( B X. _V ) )
5	2, 3, 4	3eqtr4g 2142	1 |- ( A = B -> ( C |` A ) = ( C |` B ) )

Syntax hints:   -> wi 4   = wceq 1287   _Vcvv 2615   i^i cin 2987   X. cxp 4411   |` cres 4415

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-in 2994  df-opab 3877  df-xp 4419  df-res 4425

This theorem is referenced by:  reseq2i  4680  reseq2d  4683  resabs1  4711  resima2  4715  imaeq2  4739  resdisj  4827  relcoi1  4930  fressnfv  5449  tfrlem1  6029  tfrlem9  6040  tfr0dm  6043  tfrlemisucaccv  6046  tfrlemiubacc  6051  tfr1onlemsucaccv  6062  tfr1onlemubacc  6067  tfr1onlemaccex  6069  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllemubacc  6080  tfrcllemaccex  6082  tfrcllemres  6083  tfrcldm  6084  fnfi  6599