Description: An alternate way of defining a transitive class. Definition of Enderton p. 71. (Contributed by NM, 29-Aug-1993)
Ref | Expression | ||
---|---|---|---|
Assertion | dftr4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-tr | |
|
2 | sspwuni | |
|
3 | 1 2 | bitr4i | |