Definition df-tr 4088

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4089 (which is suggestive of the word "transitive"), dftr3 4091, dftr4 4092, and dftr5 4090. 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 4087	. 2 wff Tr 𝐴
3	1	cuni 3796	. . 3 class ∪ 𝐴
4	3, 1	wss 3121	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 104	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  4089  dftr4  4092  treq  4093  trv  4099  pwtr  4204  unisuc  4398  unisucg  4399  orduniss  4410