Definition df-tr 3855

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3856 (which is suggestive of the word "transitive"), dftr3 3858, dftr4 3859, and dftr5 3857. 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 3854	. 2 wff Tr 𝐴
3	1	cuni 3580	. . 3 class ∪ 𝐴
4	3, 1	wss 2917	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 98	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  3856  dftr4  3859  treq  3860  trv  3866  pwtr  3955  unisuc  4150  unisucg  4151  orduniss  4162