Metamath Proof Explorer

Theorem reseq1

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

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

Proof

Step Hyp Ref Expression
1 ineq1 
 |-  ( A = B -> ( A i^i ( C X. _V ) ) = ( B i^i ( C X. _V ) ) )
2 df-res 
 |-  ( A |` C ) = ( A i^i ( C X. _V ) )
3 df-res 
 |-  ( B |` C ) = ( B i^i ( C X. _V ) )
4 1 2 3 3eqtr4g 
 |-  ( A = B -> ( A |` C ) = ( B |` C ) )