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

Definition df-tr 3825
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3826 (which is suggestive of the word "transitive"), dftr3 3828, dftr4 3829, and dftr5 3827. 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 3824 . 2 wff Tr A
31cuni 3550 . . 3 class A
43, 1wss 2890 . 2 wff AA
52, 4wb 98 1 wff (Tr A AA)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3826  dftr4  3829  treq  3830  trv  3836  pwtr  3925  unisuc  4095  unisucg  4096  orduniss  4108
  Copyright terms: Public domain W3C validator