Definition df-tr 2676

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

This definition is referenced by:  dftr2 2677  treq 2681  trv 2687  unisuc 3041  orduniss 3071  onuninsuc 3103  trcl 4625

Copyright terms: Public domain