Definition df-tr 4214

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

This definition is referenced by:  dftr2  4215  dftr4  4218  treq  4219  trv  4225  pwtr  4340  unisuc  4539  unisucg  4540  orduniss  4551