Definition df-tr 2681

Description: Define a transitive class. Not to be confused with a transitive relation (see cotr 3436). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 2682 (which is suggestive of the word "transitive"), dftr3 2684, dftr4 2685, dftr5 2683, and (when A is a set) unisuc 3046. 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 2680	. 2 wff Tr A
3	1	cuni 2503	. . 3 class U.A
4	3, 1	wss 2047	. 2 wff U.A (_ A
5	2, 4	wb 146	1 wff (Tr A <-> U.A (_ A)

This definition is referenced by:  dftr2 2682  treq 2686  trv 2692  unisuc 3046  orduniss 3076  onuninsuc 3108  trcl 4645

Copyright terms: Public domain