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

Definition df-tr 4114
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 4115 (which is suggestive of the word "transitive"), dftr3 4117, dftr4 4118, dftr5 4116, 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 4113 . 2  wff  Tr  A
31cuni 3827 . . 3  class  U. A
43, 1wss 3152 . 2  wff  U. A  C_  A
52, 4wb 176 1  wff  ( Tr  A  <->  U. A  C_  A
)
Colors of variables: wff set class
This definition is referenced by:  dftr2  4115  dftr4  4118  treq  4119  trv  4125  pwtr  4226  unisuc  4468  orduniss  4487  onuninsuci  4631  trcl  7410  tc2  7427  r1tr2  7449  tskuni  8405  untangtr  24060  hfuni  24814  inttrp  25108  trunitr  25109
  Copyright terms: Public domain W3C validator