Definition df-tr 4103

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4104 (which is suggestive of the word "transitive"), dftr3 4106, dftr4 4107, and dftr5 4105. 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 4102	. 2 wff Tr A
3	1	cuni 3810	. . 3 class U. A
4	3, 1	wss 3130	. 2 wff U. A C_ A
5	2, 4	wb 105	1 wff ( Tr A <-> U. A C_ A )

This definition is referenced by:  dftr2  4104  dftr4  4107  treq  4108  trv  4114  pwtr  4220  unisuc  4414  unisucg  4415  orduniss  4426