ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-tr Structured version   GIF version

Definition df-tr 3846
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3847 (which is suggestive of the word "transitive"), dftr3 3849, dftr4 3850, and dftr5 3848. 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 A AA)

Detailed syntax breakdown of Definition df-tr
StepHypRef Expression
1 cA . . 3 class A
21wtr 3845 . 2 wff Tr A
31cuni 3571 . . 3 class A
43, 1wss 2911 . 2 wff AA
52, 4wb 98 1 wff (Tr A AA)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3847  dftr4  3850  treq  3851  trv  3857  pwtr  3946  unisuc  4116  unisucg  4117  orduniss  4128
  Copyright terms: Public domain W3C validator