| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-tr | Structured version Visualization version GIF version | ||
| Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6130). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5261 (which is suggestive of the word "transitive"), dftr2c 5262, dftr3 5265, dftr4 5266, dftr5 5263, and (when 𝐴 is a set) unisuc 6463. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
| Ref | Expression |
|---|---|
| df-tr | ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | 1 | wtr 5259 | . 2 wff Tr 𝐴 |
| 3 | 1 | cuni 4907 | . . 3 class ∪ 𝐴 |
| 4 | 3, 1 | wss 3951 | . 2 wff ∪ 𝐴 ⊆ 𝐴 |
| 5 | 2, 4 | wb 206 | 1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dftr2 5261 dftr4 5266 treq 5267 trv 5273 pwtr 5457 unisucg 6462 orduniss 6481 onuninsuci 7861 trcl 9768 tc2 9782 r1tr2 9817 tskuni 10823 untangtr 35714 hfuni 36185 |
| Copyright terms: Public domain | W3C validator |