Definition df-tr 4753

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5508). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4754 (which is suggestive of the word "transitive"), dftr3 4756, dftr4 4757, dftr5 4755, and (when A is a set) unisuc 5801. 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wtr 4752	. 2 wff Tr A
3	1	cuni 4436	. . 3 class U. A
4	3, 1	wss 3574	. 2 wff U. A C_ A
5	2, 4	wb 196	1 wff ( Tr A <-> U. A C_ A )

This definition is referenced by:  dftr2  4754  dftr4  4757  treq  4758  trv  4765  pwtr  4921  unisuc  5801  orduniss  5821  onuninsuci  7040  trcl  8604  tc2  8618  r1tr2  8640  tskuni  9605  untangtr  31591  hfuni  32291