Definition df-symrels

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 . Alternate definitions are dfsymrels2 , dfsymrels3 , dfsymrels4 and dfsymrels5 .

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csymrels	⊢ SymRels
1		csyms	⊢ Syms
2		crels	⊢ Rels
3	1 2	cin	⊢ ( Syms ∩ Rels )
4	0 3	wceq	⊢ SymRels = ( Syms ∩ Rels )