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

Definition df-tr 4295
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5238). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4296 (which is suggestive of the word "transitive"), dftr3 4298, dftr4 4299, dftr5 4297, and (when  A is a set) unisuc 4649. 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 4294 . 2  wff  Tr  A
31cuni 4007 . . 3  class  U. A
43, 1wss 3312 . 2  wff  U. A  C_  A
52, 4wb 177 1  wff  ( Tr  A  <->  U. A  C_  A
)
Colors of variables: wff set class
This definition is referenced by:  dftr2  4296  dftr4  4299  treq  4300  trv  4306  pwtr  4408  unisuc  4649  orduniss  4668  onuninsuci  4812  trcl  7656  tc2  7673  r1tr2  7695  tskuni  8650  untangtr  25155  hfuni  26117
  Copyright terms: Public domain W3C validator