Description: Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | predel | |- ( Y e. Pred ( R , A , X ) -> Y e. A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elinel1 | |- ( Y e. ( A i^i ( `' R " { X } ) ) -> Y e. A ) |
|
2 | df-pred | |- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) ) |
|
3 | 1 2 | eleq2s | |- ( Y e. Pred ( R , A , X ) -> Y e. A ) |