Definition df-tr 4159

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4160 (which is suggestive of the word "transitive"), dftr3 4162, dftr4 4163, and dftr5 4161. 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 4158	. 2 wff Tr 𝐴
3	1	cuni 3864	. . 3 class ∪ 𝐴
4	3, 1	wss 3174	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 105	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  4160  dftr4  4163  treq  4164  trv  4170  pwtr  4281  unisuc  4478  unisucg  4479  orduniss  4490