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

Definition df-tr 4102
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4103 (which is suggestive of the word "transitive"), dftr3 4105, dftr4 4106, and dftr5 4104. 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 4101 . 2  wff  Tr  A
31cuni 3809 . . 3  class  U. A
43, 1wss 3129 . 2  wff  U. A  C_  A
52, 4wb 105 1  wff  ( Tr  A  <->  U. A  C_  A
)
Colors of variables: wff set class
This definition is referenced by:  dftr2  4103  dftr4  4106  treq  4107  trv  4113  pwtr  4219  unisuc  4413  unisucg  4414  orduniss  4425
  Copyright terms: Public domain W3C validator