Definition df-tr 5218

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6111). 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 used by:  dftr2  5219  dftr4  5223  treq  5224  trv  5231  pwtr  5432  unisucg  6441  orduniss  6460  onuninsuci  7834  trcl  9695  tc2  9707  r1tr2  9747  tskuni  10774  tz9.1regs  35555  untangtr  36214  hfuni  36684  ttctr3  37034  ttcmin  37035  ttcuniun  37049  ttcuni  37052