Metamath Proof Explorer


Definition df-tr

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr ). Definition of Enderton p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 (which is suggestive of the word "transitive"), dftr3 , dftr4 , dftr5 , and (when A is a set) unisuc . The term "complete" is used instead of "transitive" in Definition 3 of Suppes p. 130. (Contributed by NM, 29-Aug-1993)

Ref Expression
Assertion df-tr
|- ( Tr A <-> U. A C_ A )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 0 wtr
 |-  Tr A
2 0 cuni
 |-  U. A
3 2 0 wss
 |-  U. A C_ A
4 1 3 wb
 |-  ( Tr A <-> U. A C_ A )