Step |
Hyp |
Ref |
Expression |
1 |
|
in0 |
|- ( A i^i (/) ) = (/) |
2 |
|
incom |
|- ( A i^i (/) ) = ( (/) i^i A ) |
3 |
1 2
|
eqtr3i |
|- (/) = ( (/) i^i A ) |
4 |
|
0ex |
|- (/) e. _V |
5 |
|
eleq1 |
|- ( x = (/) -> ( x e. X <-> (/) e. X ) ) |
6 |
|
ineq1 |
|- ( x = (/) -> ( x i^i A ) = ( (/) i^i A ) ) |
7 |
6
|
eqeq2d |
|- ( x = (/) -> ( (/) = ( x i^i A ) <-> (/) = ( (/) i^i A ) ) ) |
8 |
5 7
|
anbi12d |
|- ( x = (/) -> ( ( x e. X /\ (/) = ( x i^i A ) ) <-> ( (/) e. X /\ (/) = ( (/) i^i A ) ) ) ) |
9 |
4 8
|
spcev |
|- ( ( (/) e. X /\ (/) = ( (/) i^i A ) ) -> E. x ( x e. X /\ (/) = ( x i^i A ) ) ) |
10 |
3 9
|
mpan2 |
|- ( (/) e. X -> E. x ( x e. X /\ (/) = ( x i^i A ) ) ) |
11 |
|
df-rex |
|- ( E. x e. X (/) = ( x i^i A ) <-> E. x ( x e. X /\ (/) = ( x i^i A ) ) ) |
12 |
10 11
|
sylibr |
|- ( (/) e. X -> E. x e. X (/) = ( x i^i A ) ) |
13 |
|
elrest |
|- ( ( X e. V /\ A e. W ) -> ( (/) e. ( X |`t A ) <-> E. x e. X (/) = ( x i^i A ) ) ) |
14 |
12 13
|
syl5ibr |
|- ( ( X e. V /\ A e. W ) -> ( (/) e. X -> (/) e. ( X |`t A ) ) ) |