![]() |
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 3879 (which is suggestive of the word "transitive"), dftr3 3881, dftr4 3882, and dftr5 3880. 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 3877 | . 2 wff Tr 𝐴 |
3 | 1 | cuni 3603 | . . 3 class ∪ 𝐴 |
4 | 3, 1 | wss 2974 | . 2 wff ∪ 𝐴 ⊆ 𝐴 |
5 | 2, 4 | wb 103 | 1 wff (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) |
Colors of variables: wff set class |
This definition is referenced by: dftr2 3879 dftr4 3882 treq 3883 trv 3889 pwtr 3976 unisuc 4170 unisucg 4171 orduniss 4182 |
Copyright terms: Public domain | W3C validator |