![]() |
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 4118 (which is suggestive of the word "transitive"), dftr3 4120, dftr4 4121, and dftr5 4119. 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 4116 |
. 2
![]() ![]() ![]() |
3 | 1 | cuni 3824 |
. . 3
![]() ![]() ![]() |
4 | 3, 1 | wss 3144 |
. 2
![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dftr2 4118 dftr4 4121 treq 4122 trv 4128 pwtr 4237 unisuc 4431 unisucg 4432 orduniss 4443 |
Copyright terms: Public domain | W3C validator |