Theorem resdmdfsn

Description: Restricting a class to its domain without a set is the same as restricting the class to the universe without this set. (Contributed by AV, 2-Dec-2018) Remove antecedent. (Revised by Eric Schmidt, 16-Jun-2026)

	Ref	Expression
Assertion	resdmdfsn	⊢ ( 𝑅 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝑅 ↾ ( dom 𝑅 ∖ { 𝑋 } ) )

Proof

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