Definition df-tr 5218

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6112). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5219 (which is suggestive of the word "transitive"), dftr2c 5220, dftr3 5222, dftr4 5223, dftr5 5221, and (when 𝐴 is a set) unisuc 6442. 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 5217	. 2 wff Tr 𝐴
3	1	cuni 4871	. . 3 class ∪ 𝐴
4	3, 1	wss 3904	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 209	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  5219  dftr4  5223  treq  5224  trv  5231  pwtr  5433  unisucg  6441  orduniss  6460  onuninsuci  7835  trcl  9696  tc2  9708  r1tr2  9748  tskuni  10767  tz9.1regs  35501  untangtr  36160  hfuni  36630  ttctr3  36950  ttcmin  36951  ttcuniun  36965  ttcuni  36968