Definition df-tr 4144

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4145 (which is suggestive of the word "transitive"), dftr3 4147, dftr4 4148, and dftr5 4146. 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 4143	. 2 wff Tr A
3	1	cuni 3850	. . 3 class U. A
4	3, 1	wss 3166	. 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  4145  dftr4  4148  treq  4149  trv  4155  pwtr  4264  unisuc  4461  unisucg  4462  orduniss  4473