Definition df-tr 5194

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6073). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5195 (which is suggestive of the word "transitive"), dftr2c 5196, dftr3 5198, dftr4 5199, dftr5 5197, and (when 𝐴 is a set) unisuc 6402. 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 5193	. 2 wff Tr 𝐴
3	1	cuni 4851	. . 3 class ∪ 𝐴
4	3, 1	wss 3890	. 2 wff ∪ 𝐴 ⊆ 𝐴
5	2, 4	wb 206	1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)

This definition is referenced by:  dftr2  5195  dftr4  5199  treq  5200  trv  5207  pwtr  5403  unisucg  6401  orduniss  6420  onuninsuci  7788  trcl  9646  tc2  9658  r1tr2  9698  tskuni  10703  tz9.1regs  35275  untangtr  35893  hfuni  36363  ttctr3  36674  ttcmin  36675  ttcuniun  36689  ttcuni  36692