Definition df-tr 4182

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

This definition is referenced by:  dftr2  4183  dftr4  4186  treq  4187  trv  4193  pwtr  4304  unisuc  4503  unisucg  4504  orduniss  4515