Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-tr | GIF version |
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4076 (which is suggestive of the word "transitive"), dftr3 4078, dftr4 4079, and dftr5 4077. 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 4074 | . 2 wff Tr 𝐴 |
3 | 1 | cuni 3783 | . . 3 class ∪ 𝐴 |
4 | 3, 1 | wss 3111 | . 2 wff ∪ 𝐴 ⊆ 𝐴 |
5 | 2, 4 | wb 104 | 1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) |
Colors of variables: wff set class |
This definition is referenced by: dftr2 4076 dftr4 4079 treq 4080 trv 4086 pwtr 4191 unisuc 4385 unisucg 4386 orduniss 4397 |
Copyright terms: Public domain | W3C validator |