Metamath Proof Explorer


Theorem elpredgg

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011) Generalize to closed form. (Revised by BJ, 16-Oct-2024)

Ref Expression
Assertion elpredgg
|- ( ( X e. V /\ Y e. W ) -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) )

Proof

Step Hyp Ref Expression
1 df-pred
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
2 1 elin2
 |-  ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y e. ( `' R " { X } ) ) )
3 elinisegg
 |-  ( ( X e. V /\ Y e. W ) -> ( Y e. ( `' R " { X } ) <-> Y R X ) )
4 3 anbi2d
 |-  ( ( X e. V /\ Y e. W ) -> ( ( Y e. A /\ Y e. ( `' R " { X } ) ) <-> ( Y e. A /\ Y R X ) ) )
5 2 4 bitrid
 |-  ( ( X e. V /\ Y e. W ) -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) )