Definition df-symrels 39557

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 39575. Alternate definitions are dfsymrels2 39559, dfsymrels3 39560, dfsymrels4 39565 and dfsymrels5 39566.

This definition is similar to the definitions of the classes of reflexive (df-refrels 39525) and transitive (df-trrels 39591) 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 39128	. 2 class SymRels
2		csyms 39127	. . 3 class Syms
3		crels 39119	. . 3 class Rels
4	2, 3	cin 3898	. 2 class ( Syms ∩ Rels )
5	1, 4	wceq 1570	1 wff SymRels = ( Syms ∩ Rels )

This definition is used by:  dfsymrels2  39559