Theorem dfsymrel2

Description: Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 19-Apr-2019) (Revised by Peter Mazsa, 17-Aug-2021)

	Ref	Expression
Assertion	dfsymrel2	|- ( SymRel R <-> ( `' R C_ R /\ Rel R ) )

Proof

Step	Hyp	Ref	Expression
1		df-symrel	|- ( SymRel R <-> ( `' ( R 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	cnveqd	|- ( Rel R -> `' ( R i^i ( dom R X. ran R ) ) = `' R )
5	4 3	sseq12d	|- ( Rel R -> ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) <-> `' R C_ R ) )
6	5	pm5.32ri	|- ( ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) <-> ( `' R C_ R /\ Rel R ) )
7	1 6	bitri	|- ( SymRel R <-> ( `' R C_ R /\ Rel R ) )