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 Rels

Detailed syntax breakdown

Step Hyp Ref Expression
0 csymrels class SymRels
1 csyms class Syms
2 crels class Rels
3 1 2 cin class Syms Rels
4 0 3 wceq wff SymRels = Syms Rels