Description: Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012) (Proof shortened by BJ, 16-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elpredim.1 | |- X e. _V |
|
Assertion | elpredim | |- ( Y e. Pred ( R , A , X ) -> Y R X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpredim.1 | |- X e. _V |
|
2 | elpredimg | |- ( ( X e. _V /\ Y e. Pred ( R , A , X ) ) -> Y R X ) |
|
3 | 1 2 | mpan | |- ( Y e. Pred ( R , A , X ) -> Y R X ) |