Metamath Proof Explorer


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 i^i Rels )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csymrels
 |-  SymRels
1 csyms
 |-  Syms
2 crels
 |-  Rels
3 1 2 cin
 |-  ( Syms i^i Rels )
4 0 3 wceq
 |-  SymRels = ( Syms i^i Rels )