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

Definition df-tr 3878
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3879 (which is suggestive of the word "transitive"), dftr3 3881, dftr4 3882, and dftr5 3880. 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 3877 . 2 wff Tr 𝐴
31cuni 3603 . . 3 class 𝐴
43, 1wss 2974 . 2 wff 𝐴𝐴
52, 4wb 103 1 wff (Tr 𝐴 𝐴𝐴)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3879  dftr4  3882  treq  3883  trv  3889  pwtr  3976  unisuc  4170  unisucg  4171  orduniss  4182
  Copyright terms: Public domain W3C validator