Definition df-tr 4193

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

This definition is referenced by:  dftr2  4194  dftr4  4197  treq  4198  trv  4204  pwtr  4317  unisuc  4516  unisucg  4517  orduniss  4528