Step |
Hyp |
Ref |
Expression |
1 |
|
elrestd.1 |
|- ( ph -> J e. V ) |
2 |
|
elrestd.2 |
|- ( ph -> B e. W ) |
3 |
|
elrestd.3 |
|- ( ph -> X e. J ) |
4 |
|
elrestd.4 |
|- A = ( X i^i B ) |
5 |
4
|
a1i |
|- ( ph -> A = ( X i^i B ) ) |
6 |
|
ineq1 |
|- ( x = X -> ( x i^i B ) = ( X i^i B ) ) |
7 |
6
|
rspceeqv |
|- ( ( X e. J /\ A = ( X i^i B ) ) -> E. x e. J A = ( x i^i B ) ) |
8 |
3 5 7
|
syl2anc |
|- ( ph -> E. x e. J A = ( x i^i B ) ) |
9 |
|
elrest |
|- ( ( J e. V /\ B e. W ) -> ( A e. ( J |`t B ) <-> E. x e. J A = ( x i^i B ) ) ) |
10 |
1 2 9
|
syl2anc |
|- ( ph -> ( A e. ( J |`t B ) <-> E. x e. J A = ( x i^i B ) ) ) |
11 |
8 10
|
mpbird |
|- ( ph -> A e. ( J |`t B ) ) |