Definition df-tr 4211

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

This definition is referenced by:  dftr2  4212  dftr4  4215  treq  4216  trv  4222  pwtr  4337  unisuc  4536  unisucg  4537  orduniss  4548