Definition df-tr 3878

Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3879 (which is suggestive of the word "transitive"), dftr3 3881, dftr4 3882, and dftr5 3880. 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 3877	. 2 wff Tr 𝐴
3	1	cuni 3603	. . 3 class ∪ 𝐴
4	3, 1	wss 2974	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 103	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  3879  dftr4  3882  treq  3883  trv  3889  pwtr  3976  unisuc  4170  unisucg  4171  orduniss  4182