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

Definition df-tr 3882
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3883 (which is suggestive of the word "transitive"), dftr3 3885, dftr4 3886, and dftr5 3884. 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 3881 . 2  wff  Tr  A
31cuni 3607 . . 3  class  U. A
43, 1wss 2944 . 2  wff  U. A  C_  A
52, 4wb 102 1  wff  ( Tr  A  <->  U. A  C_  A
)
Colors of variables: wff set class
This definition is referenced by:  dftr2  3883  dftr4  3886  treq  3887  trv  3893  pwtr  3982  unisuc  4177  unisucg  4178  orduniss  4189
  Copyright terms: Public domain W3C validator