MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tr Unicode version

Definition df-tr 4130
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5071). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4131 (which is suggestive of the word "transitive"), dftr3 4133, dftr4 4134, dftr5 4132, and (when  A is a set) unisuc 4484. 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 4129 . 2  wff  Tr  A
31cuni 3843 . . 3  class  U. A
43, 1wss 3165 . 2  wff  U. A  C_  A
52, 4wb 176 1  wff  ( Tr  A  <->  U. A  C_  A
)
Colors of variables: wff set class
This definition is referenced by:  dftr2  4131  dftr4  4134  treq  4135  trv  4141  pwtr  4242  unisuc  4484  orduniss  4503  onuninsuci  4647  trcl  7426  tc2  7443  r1tr2  7465  tskuni  8421  untangtr  24075  hfuni  24886  inttrp  25211  trunitr  25212
  Copyright terms: Public domain W3C validator