Definition df-tr 4027

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4028 (which is suggestive of the word "transitive"), dftr3 4030, dftr4 4031, and dftr5 4029. 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 4026	. 2 wff Tr A
3	1	cuni 3736	. . 3 class U. A
4	3, 1	wss 3071	. 2 wff U. A C_ A
5	2, 4	wb 104	1 wff ( Tr A <-> U. A C_ A )

This definition is referenced by:  dftr2  4028  dftr4  4031  treq  4032  trv  4038  pwtr  4141  unisuc  4335  unisucg  4336  orduniss  4347