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 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
StepHypRef Expression
1 csymrels 34473 . 2 class SymRels
2 csyms 34472 . . 3 class Syms
3 crels 34464 . . 3 class Rels
42, 3cin 3767 . 2 class ( Syms ∩ Rels )
51, 4wceq 1653 1 wff SymRels = ( Syms ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfsymrels2  34778
  Copyright terms: Public domain W3C validator