Definition df-symrels 36584

Description: Define the class of symmetric relations. For sets, being an element of the class of symmetric relations is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 36598. Alternate definitions are dfsymrels2 36586, dfsymrels3 36587, dfsymrels4 36588 and dfsymrels5 36589.

This definition is similar to the definitions of the classes of reflexive (df-refrels 36556) and transitive (df-trrels 36614) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)

Assertion

Ref	Expression
df-symrels	⊢ SymRels = ( Syms ∩ Rels )

Detailed syntax breakdown of Definition df-symrels

Step	Hyp	Ref	Expression
1		csymrels 36271	. 2 class SymRels
2		csyms 36270	. . 3 class Syms
3		crels 36262	. . 3 class Rels
4	2, 3	cin 3882	. 2 class ( Syms ∩ Rels )
5	1, 4	wceq 1539	1 wff SymRels = ( Syms ∩ Rels )

This definition is referenced by:  dfsymrels2  36586