Definition df-tr 3912

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3913 (which is suggestive of the word "transitive"), dftr3 3915, dftr4 3916, and dftr5 3914. 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 3911	. 2 wff Tr A
3	1	cuni 3636	. . 3 class U. A
4	3, 1	wss 2988	. 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  3913  dftr4  3916  treq  3917  trv  3923  pwtr  4020  unisuc  4214  unisucg  4215  orduniss  4226