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 𝑅 → ( 𝑅 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝑅 ↾ ( dom 𝑅 ∖ { 𝑋 } ) ) )

Proof

Step Hyp Ref Expression
1 resindm ⊢ ( Rel 𝑅 → ( 𝑅 ↾ ( ( V ∖ { 𝑋 } ) ∩ dom 𝑅 ) ) = ( 𝑅 ↾ ( V ∖ { 𝑋 } ) ) )
2 indif1 ⊢ ( ( V ∖ { 𝑋 } ) ∩ dom 𝑅 ) = ( ( V ∩ dom 𝑅 ) ∖ { 𝑋 } )
3 incom ⊢ ( V ∩ dom 𝑅 ) = ( dom 𝑅 ∩ V )
4 inv1 ⊢ ( dom 𝑅 ∩ V ) = dom 𝑅
5 3 4 eqtri ⊢ ( V ∩ dom 𝑅 ) = dom 𝑅
6 5 difeq1i ⊢ ( ( V ∩ dom 𝑅 ) ∖ { 𝑋 } ) = ( dom 𝑅 ∖ { 𝑋 } )
7 2 6 eqtri ⊢ ( ( V ∖ { 𝑋 } ) ∩ dom 𝑅 ) = ( dom 𝑅 ∖ { 𝑋 } )
8 7 reseq2i ⊢ ( 𝑅 ↾ ( ( V ∖ { 𝑋 } ) ∩ dom 𝑅 ) ) = ( 𝑅 ↾ ( dom 𝑅 ∖ { 𝑋 } ) )
9 1 8 eqtr3di ⊢ ( Rel 𝑅 → ( 𝑅 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝑅 ↾ ( dom 𝑅 ∖ { 𝑋 } ) ) )