Definition df-tr 4230

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

This definition is used by:  dftr2  4231  dftr4  4234  treq  4235  trv  4241  pwtr  4359  unisuc  4558  unisucg  4559  orduniss  4570