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

Definition df-tr 4116
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5055). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4117 (which is suggestive of the word "transitive"), dftr3 4119, dftr4 4120, dftr5 4118, and (when  A is a set) unisuc 4468. 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 4115 . 2  wff  Tr  A
31cuni 3829 . . 3  class  U. A
43, 1wss 3154 . 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  4117  dftr4  4120  treq  4121  trv  4127  pwtr  4226  unisuc  4468  orduniss  4487  onuninsuci  4631  trcl  7406  tc2  7423  r1tr2  7445  tskuni  8401  untangtr  23465  hfuni  24222  inttrp  24507  trunitr  24508
  Copyright terms: Public domain W3C validator