Metamath Proof Explorer


Theorem predbrg

Description: Closed form of elpredim . (Contributed by Scott Fenton, 13-Apr-2011) (Revised by NM, 5-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 predeq3
 |-  ( x = X -> Pred ( R , A , x ) = Pred ( R , A , X ) )
2 1 eleq2d
 |-  ( x = X -> ( Y e. Pred ( R , A , x ) <-> Y e. Pred ( R , A , X ) ) )
3 breq2
 |-  ( x = X -> ( Y R x <-> Y R X ) )
4 2 3 imbi12d
 |-  ( x = X -> ( ( Y e. Pred ( R , A , x ) -> Y R x ) <-> ( Y e. Pred ( R , A , X ) -> Y R X ) ) )
5 vex
 |-  x e. _V
6 5 elpredim
 |-  ( Y e. Pred ( R , A , x ) -> Y R x )
7 4 6 vtoclg
 |-  ( X e. V -> ( Y e. Pred ( R , A , X ) -> Y R X ) )
8 7 imp
 |-  ( ( X e. V /\ Y e. Pred ( R , A , X ) ) -> Y R X )