Definition df-symrels 34776

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, cf. elsymrelsrel 34790. Alternate definitions are dfsymrels2 34778, dfsymrels3 34779, dfsymrels4 34780 and dfsymrels5 34781.

This definition is similar to the definitions of the classes of reflexive (df-refrels 34748) and transitive (df-trrels 34806) 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 34473	. 2 class SymRels
2		csyms 34472	. . 3 class Syms
3		crels 34464	. . 3 class Rels
4	2, 3	cin 3767	. 2 class ( Syms ∩ Rels )
5	1, 4	wceq 1653	1 wff SymRels = ( Syms ∩ Rels )

This definition is referenced by:  dfsymrels2  34778