Definition df-tr 4129

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4130 (which is suggestive of the word "transitive"), dftr3 4132, dftr4 4133, and dftr5 4131. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)

Assertion

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

Detailed syntax breakdown of Definition df-tr

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wtr 4128	. 2 wff Tr 𝐴
3	1	cuni 3836	. . 3 class ∪ 𝐴
4	3, 1	wss 3154	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 105	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  4130  dftr4  4133  treq  4134  trv  4140  pwtr  4249  unisuc  4445  unisucg  4446  orduniss  4457