Metamath Proof Explorer

Theorem elpred

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011) (Proof shortened by BJ, 16-Oct-2024)

Ref Expression
Hypothesis elpred.1 
|- Y e. _V
Assertion elpred 
|- ( X e. D -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) )

Proof

Step Hyp Ref Expression
1 elpred.1 
 |-  Y e. _V
2 elpredgg 
 |-  ( ( X e. D /\ Y e. _V ) -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) )
3 1 2 mpan2 
 |-  ( X e. D -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) )