Definition df-tr 4232

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4233 (which is suggestive of the word "transitive"), dftr3 4235, dftr4 4236, and dftr5 4234. 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 4231	. 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  4233  dftr4  4236  treq  4237  trv  4243  pwtr  4361  unisuc  4560  unisucg  4561  orduniss  4572