![]() |
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 3906 (which is suggestive of the word "transitive"), dftr3 3908, dftr4 3909, and dftr5 3907. 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 3904 |
. 2
![]() ![]() ![]() |
3 | 1 | cuni 3630 |
. . 3
![]() ![]() ![]() |
4 | 3, 1 | wss 2986 |
. 2
![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | wb 103 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dftr2 3906 dftr4 3909 treq 3910 trv 3916 pwtr 4013 unisuc 4207 unisucg 4208 orduniss 4219 |
Copyright terms: Public domain | W3C validator |