Metamath Proof Explorer

Theorem elpredg

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

Ref Expression
Assertion elpredg 
|- ( ( X e. B /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) <-> Y R X ) )

Proof

Step Hyp Ref Expression
1 elpredgg 
 |-  ( ( X e. B /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) )
2 ibar 
 |-  ( Y e. A -> ( Y R X <-> ( Y e. A /\ Y R X ) ) )
3 2 bicomd 
 |-  ( Y e. A -> ( ( Y e. A /\ Y R X ) <-> Y R X ) )
4 3 adantl 
 |-  ( ( X e. B /\ Y e. A ) -> ( ( Y e. A /\ Y R X ) <-> Y R X ) )
5 1 4 bitrd 
 |-  ( ( X e. B /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) <-> Y R X ) )