Definition df-tr 4097

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

This definition is referenced by:  dftr2  4098  dftr4  4101  treq  4102  trv  4108  pwtr  4213  unisuc  4407  unisucg  4408  orduniss  4419