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 4087 (which is suggestive of the word "transitive"), dftr3 4089, dftr4 4090, and dftr5 4088. 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 4085 | . 2 |
3 | 1 | cuni 3794 | . . 3 |
4 | 3, 1 | wss 3121 | . 2 |
5 | 2, 4 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dftr2 4087 dftr4 4090 treq 4091 trv 4097 pwtr 4202 unisuc 4396 unisucg 4397 orduniss 4408 |
Copyright terms: Public domain | W3C validator |