Definition df-tr 4188

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

This definition is referenced by:  dftr2  4189  dftr4  4192  treq  4193  trv  4199  pwtr  4311  unisuc  4510  unisucg  4511  orduniss  4522