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

Definition df-tr 4054
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5008). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4055 (which is suggestive of the word "transitive"), dftr3 4057, dftr4 4058, dftr5 4056, and (when  A is a set) unisuc 4405. 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 4053 . 2  wff  Tr  A
31cuni 3768 . . 3  class  U. A
43, 1wss 3094 . 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  4055  dftr4  4058  treq  4059  trv  4065  pwtr  4164  unisuc  4405  orduniss  4424  onuninsuci  4568  trcl  7343  tc2  7360  r1tr2  7382  tskuni  8338  untangtr  23397  hfuni  24154  inttrp  24439  trunitr  24440
  Copyright terms: Public domain W3C validator