Definition df-tr 4086

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4087 (which is suggestive of the word "transitive"), dftr3 4089, dftr4 4090, and dftr5 4088. 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 4085	. 2 wff Tr A
3	1	cuni 3794	. . 3 class U. A
4	3, 1	wss 3121	. 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  4087  dftr4  4090  treq  4091  trv  4097  pwtr  4202  unisuc  4396  unisucg  4397  orduniss  4408