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

Definition df-tr 3818
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3819 (which is suggestive of the word "transitive"), dftr3 3821, dftr4 3822, and dftr5 3820. 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 3817 . 2 wff Tr A
31cuni 3543 . . 3 class A
43, 1wss 2885 . 2 wff AA
52, 4wb 98 1 wff (Tr A AA)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3819  dftr4  3822  treq  3823  trv  3829  pwtr  3918  unisuc  4088  unisucg  4089  orduniss  4100
  Copyright terms: Public domain W3C validator