Definition df-symrel

Description: Define the symmetric relation predicate. (Read: R is a symmetric relation.) For sets, being an element of the class of symmetric relations ( df-symrels ) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel . Alternate definitions are dfsymrel2 and dfsymrel3 . (Contributed by Peter Mazsa, 16-Jul-2021)

	Ref	Expression
Assertion	df-symrel	|- ( SymRel R <-> ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1	0	wsymrel	|- SymRel R
2	0	cdm	|- dom R
3	0	crn	|- ran R
4	2 3	cxp	|- ( dom R X. ran R )
5	0 4	cin	|- ( R i^i ( dom R X. ran R ) )
6	5	ccnv	|- `' ( R i^i ( dom R X. ran R ) )
7	6 5	wss	|- `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) )
8	0	wrel	|- Rel R
9	7 8	wa	|- ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R )
10	1 9	wb	|- ( SymRel R <-> ( `' ( R i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) )