Step |
Hyp |
Ref |
Expression |
1 |
|
shftfval.1 |
|- F e. _V |
2 |
1
|
shftfval |
|- ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } ) |
3 |
2
|
dmeqd |
|- ( A e. CC -> dom ( F shift A ) = dom { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } ) |
4 |
|
19.42v |
|- ( E. y ( x e. CC /\ ( x - A ) F y ) <-> ( x e. CC /\ E. y ( x - A ) F y ) ) |
5 |
|
ovex |
|- ( x - A ) e. _V |
6 |
5
|
eldm |
|- ( ( x - A ) e. dom F <-> E. y ( x - A ) F y ) |
7 |
6
|
anbi2i |
|- ( ( x e. CC /\ ( x - A ) e. dom F ) <-> ( x e. CC /\ E. y ( x - A ) F y ) ) |
8 |
4 7
|
bitr4i |
|- ( E. y ( x e. CC /\ ( x - A ) F y ) <-> ( x e. CC /\ ( x - A ) e. dom F ) ) |
9 |
8
|
abbii |
|- { x | E. y ( x e. CC /\ ( x - A ) F y ) } = { x | ( x e. CC /\ ( x - A ) e. dom F ) } |
10 |
|
dmopab |
|- dom { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } = { x | E. y ( x e. CC /\ ( x - A ) F y ) } |
11 |
|
df-rab |
|- { x e. CC | ( x - A ) e. dom F } = { x | ( x e. CC /\ ( x - A ) e. dom F ) } |
12 |
9 10 11
|
3eqtr4i |
|- dom { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } = { x e. CC | ( x - A ) e. dom F } |
13 |
3 12
|
eqtrdi |
|- ( A e. CC -> dom ( F shift A ) = { x e. CC | ( x - A ) e. dom F } ) |