Description: A class is a transitive predecessor iff it is in some value of the underlying function. This theorem is not meant to be used directly; use trpredpred and trpredmintr instead. (Contributed by Scott Fenton, 28-Apr-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | eltrpred | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dftrpred2 | |
|
2 | 1 | eleq2i | |
3 | eliun | |
|
4 | 2 3 | bitri | |