Theorem dfrel6

Description: Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019)

	Ref	Expression
Assertion	dfrel6	⊢ ( Rel 𝑅 ↔ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		dfrel5	⊢ ( Rel 𝑅 ↔ ( 𝑅 ↾ dom 𝑅 ) = 𝑅 )
2		dfres3	⊢ ( 𝑅 ↾ dom 𝑅 ) = ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) )
3	2	eqeq1i	⊢ ( ( 𝑅 ↾ dom 𝑅 ) = 𝑅 ↔ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) = 𝑅 )
4	1 3	bitri	⊢ ( Rel 𝑅 ↔ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) = 𝑅 )