Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-tr | Unicode version |
Description: Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 3998 (which is suggestive of the word "transitive"), dftr3 4000, dftr4 4001, and dftr5 3999. 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | wtr 3996 | . 2 |
3 | 1 | cuni 3706 | . . 3 |
4 | 3, 1 | wss 3041 | . 2 |
5 | 2, 4 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dftr2 3998 dftr4 4001 treq 4002 trv 4008 pwtr 4111 unisuc 4305 unisucg 4306 orduniss 4317 |
Copyright terms: Public domain | W3C validator |