Theorem relresfld

Description: Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012) (Proof shortened by Eric Schmidt, 16-Aug-2026)

	Ref	Expression
Assertion	relresfld	⊢ ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		relfld	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
2	1	reseq2d	⊢ ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
3		ssun1	⊢ dom 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
4		relssres	⊢ ( ( Rel 𝑅 ∧ dom 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = 𝑅 )
5	3 4	mpan2	⊢ ( Rel 𝑅 → ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = 𝑅 )
6	2 5	eqtrd	⊢ ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 )