Definition df-tr 5212

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6100). 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 6433. 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 3898	. 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  6432  orduniss  6451  onuninsuci  7834  trcl  9707  tc2  9719  r1tr2  9759  hfuniOLD  9896  tskuni  10839  tz9.1regs  35727  untangtr  36400  ttctr3  37205  ttcmin  37206  ttcuniun  37220  ttcuni  37223