Definition df-tr 3905

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3906 (which is suggestive of the word "transitive"), dftr3 3908, dftr4 3909, and dftr5 3907. 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 3904	. 2 wff Tr A
3	1	cuni 3630	. . 3 class U. A
4	3, 1	wss 2986	. 2 wff U. A C_ A
5	2, 4	wb 103	1 wff ( Tr A <-> U. A C_ A )

This definition is referenced by:  dftr2  3906  dftr4  3909  treq  3910  trv  3916  pwtr  4013  unisuc  4207  unisucg  4208  orduniss  4219