Metamath Proof Explorer

Theorem resdmdfsnOLD

Description: Obsolete version of resdmdfsn as of 16-Jun-2026. (Contributed by AV, 2-Dec-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion resdmdfsnOLD 
|- ( Rel R -> ( R |` ( _V \ { X } ) ) = ( R |` ( dom R \ { X } ) ) )

Proof

Step Hyp Ref Expression
1 resindmOLD 
 |-  ( Rel R -> ( R |` ( ( _V \ { X } ) i^i dom R ) ) = ( R |` ( _V \ { X } ) ) )
2 indif1 
 |-  ( ( _V \ { X } ) i^i dom R ) = ( ( _V i^i dom R ) \ { X } )
3 incom 
 |-  ( _V i^i dom R ) = ( dom R i^i _V )
4 inv1 
 |-  ( dom R i^i _V ) = dom R
5 3 4 eqtri 
 |-  ( _V i^i dom R ) = dom R
6 5 difeq1i 
 |-  ( ( _V i^i dom R ) \ { X } ) = ( dom R \ { X } )
7 2 6 eqtri 
 |-  ( ( _V \ { X } ) i^i dom R ) = ( dom R \ { X } )
8 7 reseq2i 
 |-  ( R |` ( ( _V \ { X } ) i^i dom R ) ) = ( R |` ( dom R \ { X } ) )
9 1 8 eqtr3di 
 |-  ( Rel R -> ( R |` ( _V \ { X } ) ) = ( R |` ( dom R \ { X } ) ) )