Definition df-symrels 39157

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 39175. Alternate definitions are dfsymrels2 39159, dfsymrels3 39160, dfsymrels4 39165 and dfsymrels5 39166.

This definition is similar to the definitions of the classes of reflexive (df-refrels 39125) and transitive (df-trrels 39191) 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 38728	. 2 class SymRels
2		csyms 38727	. . 3 class Syms
3		crels 38719	. . 3 class Rels
4	2, 3	cin 3912	. 2 class ( Syms ∩ Rels )
5	1, 4	wceq 1567	1 wff SymRels = ( Syms ∩ Rels )

This definition is referenced by:  dfsymrels2  39159