Definition df-tr 3985

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

This definition is referenced by:  dftr2  3986  dftr4  3989  treq  3990  trv  3996  pwtr  4099  unisuc  4293  unisucg  4294  orduniss  4305