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

Definition df-tr 3905
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3906 (which is suggestive of the word "transitive"), dftr3 3908, dftr4 3909, and dftr5 3907. 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 3904 . 2  wff  Tr  A
31cuni 3630 . . 3  class  U. A
43, 1wss 2986 . 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  3906  dftr4  3909  treq  3910  trv  3916  pwtr  4013  unisuc  4207  unisucg  4208  orduniss  4219
  Copyright terms: Public domain W3C validator