Definition df-tr 5182

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6068). 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 6394. 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 3884	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 208	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  5183  dftr4  5187  treq  5188  trv  5195  pwtr  5393  unisucg  6393  orduniss  6412  onuninsuci  7783  trcl  9644  tc2  9656  r1tr2  9696  tskuni  10702  tz9.1regs  35328  untangtr  35955  hfuni  36425  ttctr3  36736  ttcmin  36737  ttcuniun  36751  ttcuni  36754