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

Definition df-tr 3997
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3998 (which is suggestive of the word "transitive"), dftr3 4000, dftr4 4001, and dftr5 3999. 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 3996 . 2  wff  Tr  A
31cuni 3706 . . 3  class  U. A
43, 1wss 3041 . 2  wff  U. A  C_  A
52, 4wb 104 1  wff  ( Tr  A  <->  U. A  C_  A
)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3998  dftr4  4001  treq  4002  trv  4008  pwtr  4111  unisuc  4305  unisucg  4306  orduniss  4317
  Copyright terms: Public domain W3C validator