Metamath Proof Explorer

Theorem predel

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 )

Proof

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 )