Definition df-tr 5212

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

This definition is used by:  dftr2  5213  dftr4  5217  treq  5218  trv  5225  pwtr  5419  unisucg  6443  orduniss  6462  onuninsuci  7851  trcl  9729  tc2  9741  r1tr2  9784  hfuniOLD  9925  tskuni  10868  tz9.1regs  35844  untangtr  36521  ttctr3  37325  ttcmin  37326  ttcuniun  37340  ttcuni  37343