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

Proof

Step	Hyp	Ref	Expression
1		resindmOLD	⊢ ( 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 𝑅 ∖ { 𝑋 } ) ) )