Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-symrels Structured version   Visualization version   GIF version

Definition df-symrels 35938
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 35952. Alternate definitions are dfsymrels2 35940, dfsymrels3 35941, dfsymrels4 35942 and dfsymrels5 35943.

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

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

Detailed syntax breakdown of Definition df-symrels
StepHypRef Expression
1 csymrels 35623 . 2 class SymRels
2 csyms 35622 . . 3 class Syms
3 crels 35614 . . 3 class Rels
42, 3cin 3883 . 2 class ( Syms ∩ Rels )
51, 4wceq 1538 1 wff SymRels = ( Syms ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfsymrels2  35940
  Copyright terms: Public domain W3C validator