Definition df-tr 5216

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

This definition is used by:  dftr2  5217  dftr4  5221  treq  5222  trv  5229  pwtr  5424  unisucg  6458  orduniss  6477  onuninsuci  7872  trcl  9753  tc2  9765  r1tr2  9808  hfuniOLD  9949  tskuni  10892  tz9.1regs  35901  untangtr  36656  ttctr3  37460  ttcmin  37461  ttcuniun  37475  ttcuni  37478