Definition df-tr 5210

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6101). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5211 (which is suggestive of the word "transitive"), dftr2c 5212, dftr3 5214, dftr4 5215, dftr5 5213, and (when 𝐴 is a set) unisuc 6429. 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 5209	. 2 wff Tr 𝐴
3	1	cuni 4867	. . 3 class ∪ 𝐴
4	3, 1	wss 3906	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 208	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  5211  dftr4  5215  treq  5216  trv  5223  pwtr  5421  unisucg  6428  orduniss  6447  onuninsuci  7822  trcl  9685  tc2  9697  r1tr2  9737  tskuni  10743  tz9.1regs  35434  untangtr  36069  hfuni  36539  ttctr3  36860  ttcmin  36861  ttcuniun  36875  ttcuni  36878