Definition df-tr 4117

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4118 (which is suggestive of the word "transitive"), dftr3 4120, dftr4 4121, and dftr5 4119. 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 4116	. 2 wff Tr A
3	1	cuni 3824	. . 3 class U. A
4	3, 1	wss 3144	. 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  4118  dftr4  4121  treq  4122  trv  4128  pwtr  4237  unisuc  4431  unisucg  4432  orduniss  4443