Definition df-tr 4133

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

This definition is referenced by:  dftr2  4134  dftr4  4137  treq  4138  trv  4144  pwtr  4253  unisuc  4449  unisucg  4450  orduniss  4461