This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resdmdfsn

Description: Restricting a relation to its domain without a set is the same as restricting the relation to the universe without this set. (Contributed by AV, 2-Dec-2018)

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

Proof

Step Hyp Ref Expression
1 resindm 
 |-  ( 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 } ) ) )