Definition df-tr 4132

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

This definition is referenced by:  dftr2  4133  dftr4  4136  treq  4137  trv  4143  pwtr  4252  unisuc  4448  unisucg  4449  orduniss  4460