Definition df-tr 4228

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

This definition is referenced by:  dftr2  4229  dftr4  4232  treq  4233  trv  4239  pwtr  4357  unisuc  4556  unisucg  4557  orduniss  4568