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

Definition df-tr 4074
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5029). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4075 (which is suggestive of the word "transitive"), dftr3 4077, dftr4 4078, dftr5 4076, and (when  A is a set) unisuc 4426. 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 4073 . 2  wff  Tr  A
31cuni 3787 . . 3  class  U. A
43, 1wss 3113 . 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  4075  dftr4  4078  treq  4079  trv  4085  pwtr  4184  unisuc  4426  orduniss  4445  onuninsuci  4589  trcl  7364  tc2  7381  r1tr2  7403  tskuni  8359  untangtr  23418  hfuni  24175  inttrp  24460  trunitr  24461
  Copyright terms: Public domain W3C validator