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

Definition df-tr 3914
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3915 (which is suggestive of the word "transitive"), dftr3 3917, dftr4 3918, and dftr5 3916. 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 3913 . 2 wff Tr 𝐴
31cuni 3638 . . 3 class 𝐴
43, 1wss 2988 . 2 wff 𝐴𝐴
52, 4wb 103 1 wff (Tr 𝐴 𝐴𝐴)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3915  dftr4  3918  treq  3919  trv  3925  pwtr  4022  unisuc  4216  unisucg  4217  orduniss  4228
  Copyright terms: Public domain W3C validator