Theorem dfrefrel2

Description: Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021)

	Ref	Expression
Assertion	dfrefrel2	|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )

Proof

Step	Hyp	Ref	Expression
1		df-refrel	|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )
2		dfrel6	|- ( Rel R <-> ( R i^i ( dom R X. ran R ) ) = R )
3	2	biimpi	|- ( Rel R -> ( R i^i ( dom R X. ran R ) ) = R )
4	3	sseq2d	|- ( Rel R -> ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) <-> ( _I i^i ( dom R X. ran R ) ) C_ R ) )
5	4	pm5.32ri	|- ( ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )
6	1 5	bitri	|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )