Definition df-tr 2671

Description: Define a transitive class. Not to be confused with a transitive relation (see cotr 3420). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 2672 (which is suggestive of the word "transitive"), dftr3 2674, dftr4 2675, dftr5 2673, and (when A is a set) unisuc 3036. 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 2670	. 2 wff Tr A
3	1	cuni 2493	. . 3 class U.A
4	3, 1	wss 2037	. 2 wff U.A (_ A
5	2, 4	wb 146	1 wff (Tr A <-> U.A (_ A)

This definition is referenced by:  dftr2 2672  treq 2676  trv 2682  unisuc 3036  orduniss 3066  onuninsuc 3098  trcl 4617

Copyright terms: Public domain