Definition df-tr 4143

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

This definition is referenced by:  dftr2  4144  dftr4  4147  treq  4148  trv  4154  pwtr  4263  unisuc  4460  unisucg  4461  orduniss  4472