Definition df-tr 4186

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

This definition is referenced by:  dftr2  4187  dftr4  4190  treq  4191  trv  4197  pwtr  4309  unisuc  4508  unisucg  4509  orduniss  4520