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

Definition df-tr 3855
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3856 (which is suggestive of the word "transitive"), dftr3 3858, dftr4 3859, and dftr5 3857. 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 3854 . 2 wff Tr 𝐴
31cuni 3580 . . 3 class 𝐴
43, 1wss 2917 . 2 wff 𝐴𝐴
52, 4wb 98 1 wff (Tr 𝐴 𝐴𝐴)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3856  dftr4  3859  treq  3860  trv  3866  pwtr  3955  unisuc  4150  unisucg  4151  orduniss  4162
  Copyright terms: Public domain W3C validator