Definition df-tr 4104

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

This definition is referenced by:  dftr2  4105  dftr4  4108  treq  4109  trv  4115  pwtr  4221  unisuc  4415  unisucg  4416  orduniss  4427