Definition df-symrels 36657

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 36671. Alternate definitions are dfsymrels2 36659, dfsymrels3 36660, dfsymrels4 36661 and dfsymrels5 36662.

This definition is similar to the definitions of the classes of reflexive (df-refrels 36629) and transitive (df-trrels 36687) 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 36344	. 2 class SymRels
2		csyms 36343	. . 3 class Syms
3		crels 36335	. . 3 class Rels
4	2, 3	cin 3886	. 2 class ( Syms ∩ Rels )
5	1, 4	wceq 1539	1 wff SymRels = ( Syms ∩ Rels )

This definition is referenced by:  dfsymrels2  36659