Definition df-tr 5197

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6058). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5198 (which is suggestive of the word "transitive"), dftr2c 5199, dftr3 5201, dftr4 5202, dftr5 5200, and (when 𝐴 is a set) unisuc 6387. 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 5196	. 2 wff Tr 𝐴
3	1	cuni 4856	. . 3 class ∪ 𝐴
4	3, 1	wss 3897	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 206	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  5198  dftr4  5202  treq  5203  trv  5209  pwtr  5391  unisucg  6386  orduniss  6405  onuninsuci  7770  trcl  9618  tc2  9630  r1tr2  9670  tskuni  10674  tz9.1regs  35130  untangtr  35758  hfuni  36228