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

Definition df-tr 4117
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4118 (which is suggestive of the word "transitive"), dftr3 4120, dftr4 4121, and dftr5 4119. 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 4116 . 2  wff  Tr  A
31cuni 3824 . . 3  class  U. A
43, 1wss 3144 . 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  4118  dftr4  4121  treq  4122  trv  4128  pwtr  4237  unisuc  4431  unisucg  4432  orduniss  4443
  Copyright terms: Public domain W3C validator