MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tr Structured version   Visualization version   GIF version

Definition df-tr 4675
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5413). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4676 (which is suggestive of the word "transitive"), dftr3 4678, dftr4 4679, dftr5 4677, and (when 𝐴 is a set) unisuc 5703. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
Assertion
Ref Expression
df-tr (Tr 𝐴 𝐴𝐴)

Detailed syntax breakdown of Definition df-tr
StepHypRef Expression
1 cA . . 3 class 𝐴
21wtr 4674 . 2 wff Tr 𝐴
31cuni 4366 . . 3 class 𝐴
43, 1wss 3539 . 2 wff 𝐴𝐴
52, 4wb 194 1 wff (Tr 𝐴 𝐴𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  dftr2  4676  dftr4  4679  treq  4680  trv  4687  pwtr  4841  unisuc  5703  orduniss  5723  onuninsuci  6909  trcl  8464  tc2  8478  r1tr2  8500  tskuni  9461  untangtr  30638  hfuni  31254
  Copyright terms: Public domain W3C validator