Definition df-tr 4081

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

This definition is referenced by:  dftr2  4082  dftr4  4085  treq  4086  trv  4092  pwtr  4197  unisuc  4391  unisucg  4392  orduniss  4403