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

Definition df-tr 3912
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3913 (which is suggestive of the word "transitive"), dftr3 3915, dftr4 3916, and dftr5 3914. 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  <->  U. A  C_  A
)

Detailed syntax breakdown of Definition df-tr
StepHypRef Expression
1 cA . . 3  class  A
21wtr 3911 . 2  wff  Tr  A
31cuni 3636 . . 3  class  U. A
43, 1wss 2988 . 2  wff  U. A  C_  A
52, 4wb 103 1  wff  ( Tr  A  <->  U. A  C_  A
)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3913  dftr4  3916  treq  3917  trv  3923  pwtr  4020  unisuc  4214  unisucg  4215  orduniss  4226
  Copyright terms: Public domain W3C validator