Definition df-tr 4128

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

This definition is referenced by:  dftr2  4129  dftr4  4132  treq  4133  trv  4139  pwtr  4248  unisuc  4444  unisucg  4445  orduniss  4456