Definition df-tr 3876

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3877 (which is suggestive of the word "transitive"), dftr3 3879, dftr4 3880, and dftr5 3878. 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 3875	. 2 wff Tr A
3	1	cuni 3601	. . 3 class U. A
4	3, 1	wss 2973	. 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  3877  dftr4  3880  treq  3881  trv  3887  pwtr  3974  unisuc  4168  unisucg  4169  orduniss  4180