Theorem dfrel6

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

	Ref	Expression
Assertion	dfrel6	|- ( Rel R <-> ( R i^i ( dom R X. ran R ) ) = R )

Proof

Step	Hyp	Ref	Expression
1		dfrel5	|- ( Rel R <-> ( R |` dom R ) = R )
2		dfres3	|- ( R |` dom R ) = ( R i^i ( dom R X. ran R ) )
3	2	eqeq1i	|- ( ( R |` dom R ) = R <-> ( R i^i ( dom R X. ran R ) ) = R )
4	1 3	bitri	|- ( Rel R <-> ( R i^i ( dom R X. ran R ) ) = R )