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

Definition df-tr 4011
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 4962). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4012 (which is suggestive of the word "transitive"), dftr3 4014, dftr4 4015, dftr5 4013, and (when  A is a set) unisuc 4361. 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 4010 . 2  wff  Tr  A
31cuni 3727 . . 3  class  U. A
43, 1wss 3078 . 2  wff  U. A  C_  A
52, 4wb 178 1  wff  ( Tr  A  <->  U. A  C_  A
)
Colors of variables: wff set class
This definition is referenced by:  dftr2  4012  dftr4  4015  treq  4016  trv  4022  pwtr  4120  unisuc  4361  orduniss  4380  onuninsuci  4522  trcl  7294  tc2  7311  r1tr2  7333  tskuni  8285  untangtr  23231  hfuni  23988  inttrp  24273  trunitr  24274
  Copyright terms: Public domain W3C validator