Definition df-tr 5217

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

This definition is used by:  dftr2  5218  dftr4  5222  treq  5223  trv  5230  pwtr  5431  unisucg  6442  orduniss  6461  onuninsuci  7839  trcl  9710  tc2  9722  r1tr2  9762  tskuni  10795  tz9.1regs  35647  untangtr  36280  hfuni  36751  ttctr3  37101  ttcmin  37102  ttcuniun  37116  ttcuni  37119