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

Definition df-trrels 37529
Description: Define the class of transitive relations. For sets, being an element of the class of transitive relations is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 37537. Alternate definitions are dftrrels2 37531 and dftrrels3 37532.

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

Assertion
Ref Expression
df-trrels TrRels = ( Trs ∩ Rels )

Detailed syntax breakdown of Definition df-trrels
StepHypRef Expression
1 ctrrels 37143 . 2 class TrRels
2 ctrs 37142 . . 3 class Trs
3 crels 37131 . . 3 class Rels
42, 3cin 3947 . 2 class ( Trs ∩ Rels )
51, 4wceq 1541 1 wff TrRels = ( Trs ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dftrrels2  37531
  Copyright terms: Public domain W3C validator