Definition df-tr 5182

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6064). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5183 (which is suggestive of the word "transitive"), dftr2c 5184, dftr3 5186, dftr4 5187, dftr5 5185, and (when 𝐴 is a set) unisuc 6393. 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 5181	. 2 wff Tr 𝐴
3	1	cuni 4840	. . 3 class ∪ 𝐴
4	3, 1	wss 3885	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 206	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  5183  dftr4  5187  treq  5188  trv  5195  pwtr  5393  unisucg  6392  orduniss  6411  onuninsuci  7780  trcl  9638  tc2  9650  r1tr2  9690  tskuni  10695  tz9.1regs  35266  untangtr  35884  hfuni  36354  ttctr3  36665  ttcmin  36666  ttcuniun  36680  ttcuni  36683