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

Definition df-tr 4361
Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5182). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4362 (which is suggestive of the word "transitive"), dftr3 4364, dftr4 4365, dftr5 4363, and (when is a set) unisuc 4766. 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

Detailed syntax breakdown of Definition df-tr
StepHypRef Expression
1 cA . . 3
21wtr 4360 . 2
31cuni 4066 . . 3
43, 1wss 3305 . 2
52, 4wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  dftr2  4362  dftr4  4365  treq  4366  trv  4372  pwtr  4517  unisuc  4766  orduniss  4784  onuninsuci  6421  trcl  7895  tc2  7909  r1tr2  7931  tskuni  8896  untangtr  27067  hfuni  27924
  Copyright terms: Public domain W3C validator