Definition df-tr 4183

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4184 (which is suggestive of the word "transitive"), dftr3 4186, dftr4 4187, and dftr5 4185. 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 4182	. 2 wff Tr A
3	1	cuni 3888	. . 3 class U. A
4	3, 1	wss 3197	. 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  4184  dftr4  4187  treq  4188  trv  4194  pwtr  4305  unisuc  4504  unisucg  4505  orduniss  4516