Definition df-tr 2042

Description: Define a transitive class. Not to be confused with a transitive relation (see cotr 2625). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 2043 (which is suggestive of the word "transitive"), dftr3 2045, and dftr4 2046. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130.

Assertion

Ref	Expression
df-tr	⊢ (Tr A ↔ ∪A ⊆ A)

Detailed syntax breakdown of Definition df-tr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wtr 2041	. 2 wff Tr A
3	1	cuni 1919	. . 3 class ∪A
4	3, 1	wss 1487	. 2 wff ∪A ⊆ A
5	2, 4	wb 127	1 wff (Tr A ↔ ∪A ⊆ A)

This definition is referenced by:  dftr2 2043  treq 2047  trv 2053  unisuc 2299  orduniss 2327  onuninsuc 2356  trcl 3489

metamath.org