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 4028 (which is suggestive of the word "transitive"), dftr3 4030, dftr4 4031, and dftr5 4029. 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 4026 | . 2 |
3 | 1 | cuni 3736 | . . 3 |
4 | 3, 1 | wss 3071 | . 2 |
5 | 2, 4 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dftr2 4028 dftr4 4031 treq 4032 trv 4038 pwtr 4141 unisuc 4335 unisucg 4336 orduniss 4347 |
Copyright terms: Public domain | W3C validator |