![]() |
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 3847 (which is suggestive of the word "transitive"), dftr3 3849, dftr4 3850, and dftr5 3848. 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 A ↔ ∪ A ⊆ A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | 1 | wtr 3845 | . 2 wff Tr A |
3 | 1 | cuni 3571 | . . 3 class ∪ A |
4 | 3, 1 | wss 2911 | . 2 wff ∪ A ⊆ A |
5 | 2, 4 | wb 98 | 1 wff (Tr A ↔ ∪ A ⊆ A) |
Colors of variables: wff set class |
This definition is referenced by: dftr2 3847 dftr4 3850 treq 3851 trv 3857 pwtr 3946 unisuc 4116 unisucg 4117 orduniss 4128 |
Copyright terms: Public domain | W3C validator |