Definition df-tr 2679

Description: Define a transitive class. Not to be confused with a transitive relation (see cotr 3434). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 2680 (which is suggestive of the word "transitive"), dftr3 2682, dftr4 2683, dftr5 2681, and (when A is a set) unisuc 3044. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130.

Assertion

Ref	Expression
df-tr	|- (Tr A <-> U.A (_ A)

Detailed syntax breakdown of Definition df-tr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wtr 2678	. 2 wff Tr A
3	1	cuni 2501	. . 3 class U.A
4	3, 1	wss 2045	. 2 wff U.A (_ A
5	2, 4	wb 146	1 wff (Tr A <-> U.A (_ A)

This definition is referenced by:  dftr2 2680  treq 2684  trv 2690  unisuc 3044  orduniss 3074  onuninsuc 3106  trcl 4633

Copyright terms: Public domain