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 ) |