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		indif1	|- ( ( _V \ { X } ) i^i dom R ) = ( ( _V i^i dom R ) \ { X } )
2		incom	|- ( _V i^i dom R ) = ( dom R i^i _V )
3		inv1	|- ( dom R i^i _V ) = dom R
4	2 3	eqtri	|- ( _V i^i dom R ) = dom R
5	4	difeq1i	|- ( ( _V i^i dom R ) \ { X } ) = ( dom R \ { X } )
6	1 5	eqtri	|- ( ( _V \ { X } ) i^i dom R ) = ( dom R \ { X } )
7	6	reseq2i	|- ( R |` ( ( _V \ { X } ) i^i dom R ) ) = ( R |` ( dom R \ { X } ) )
8		resindm	|- ( Rel R -> ( R |` ( ( _V \ { X } ) i^i dom R ) ) = ( R |` ( _V \ { X } ) ) )
9	7 8	syl5reqr	|- ( Rel R -> ( R |` ( _V \ { X } ) ) = ( R |` ( dom R \ { X } ) ) )