Definition df-tr 5213

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

This definition is used by:  dftr2  5214  dftr4  5218  treq  5219  trv  5226  pwtr  5420  unisucg  6444  orduniss  6463  onuninsuci  7852  trcl  9730  tc2  9742  r1tr2  9785  hfuniOLD  9926  tskuni  10869  tz9.1regs  35803  untangtr  36480  ttctr3  37284  ttcmin  37285  ttcuniun  37299  ttcuni  37302