![]() |
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 4103 (which is suggestive of the word "transitive"), dftr3 4105, dftr4 4106, and dftr5 4104. 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 4101 |
. 2
![]() ![]() ![]() |
3 | 1 | cuni 3809 |
. . 3
![]() ![]() ![]() |
4 | 3, 1 | wss 3129 |
. 2
![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dftr2 4103 dftr4 4106 treq 4107 trv 4113 pwtr 4219 unisuc 4413 unisucg 4414 orduniss 4425 |
Copyright terms: Public domain | W3C validator |