Step |
Hyp |
Ref |
Expression |
1 |
|
df-rab |
|- { x e. CC | ( x - A ) e. B } = { x | ( x e. CC /\ ( x - A ) e. B ) } |
2 |
|
npcan |
|- ( ( x e. CC /\ A e. CC ) -> ( ( x - A ) + A ) = x ) |
3 |
2
|
ancoms |
|- ( ( A e. CC /\ x e. CC ) -> ( ( x - A ) + A ) = x ) |
4 |
3
|
eqcomd |
|- ( ( A e. CC /\ x e. CC ) -> x = ( ( x - A ) + A ) ) |
5 |
|
oveq1 |
|- ( y = ( x - A ) -> ( y + A ) = ( ( x - A ) + A ) ) |
6 |
5
|
rspceeqv |
|- ( ( ( x - A ) e. B /\ x = ( ( x - A ) + A ) ) -> E. y e. B x = ( y + A ) ) |
7 |
6
|
expcom |
|- ( x = ( ( x - A ) + A ) -> ( ( x - A ) e. B -> E. y e. B x = ( y + A ) ) ) |
8 |
4 7
|
syl |
|- ( ( A e. CC /\ x e. CC ) -> ( ( x - A ) e. B -> E. y e. B x = ( y + A ) ) ) |
9 |
8
|
expimpd |
|- ( A e. CC -> ( ( x e. CC /\ ( x - A ) e. B ) -> E. y e. B x = ( y + A ) ) ) |
10 |
9
|
adantr |
|- ( ( A e. CC /\ B C_ CC ) -> ( ( x e. CC /\ ( x - A ) e. B ) -> E. y e. B x = ( y + A ) ) ) |
11 |
|
ssel2 |
|- ( ( B C_ CC /\ y e. B ) -> y e. CC ) |
12 |
|
addcl |
|- ( ( y e. CC /\ A e. CC ) -> ( y + A ) e. CC ) |
13 |
11 12
|
sylan |
|- ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> ( y + A ) e. CC ) |
14 |
|
pncan |
|- ( ( y e. CC /\ A e. CC ) -> ( ( y + A ) - A ) = y ) |
15 |
11 14
|
sylan |
|- ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> ( ( y + A ) - A ) = y ) |
16 |
|
simplr |
|- ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> y e. B ) |
17 |
15 16
|
eqeltrd |
|- ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> ( ( y + A ) - A ) e. B ) |
18 |
13 17
|
jca |
|- ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> ( ( y + A ) e. CC /\ ( ( y + A ) - A ) e. B ) ) |
19 |
18
|
ancoms |
|- ( ( A e. CC /\ ( B C_ CC /\ y e. B ) ) -> ( ( y + A ) e. CC /\ ( ( y + A ) - A ) e. B ) ) |
20 |
19
|
anassrs |
|- ( ( ( A e. CC /\ B C_ CC ) /\ y e. B ) -> ( ( y + A ) e. CC /\ ( ( y + A ) - A ) e. B ) ) |
21 |
|
eleq1 |
|- ( x = ( y + A ) -> ( x e. CC <-> ( y + A ) e. CC ) ) |
22 |
|
oveq1 |
|- ( x = ( y + A ) -> ( x - A ) = ( ( y + A ) - A ) ) |
23 |
22
|
eleq1d |
|- ( x = ( y + A ) -> ( ( x - A ) e. B <-> ( ( y + A ) - A ) e. B ) ) |
24 |
21 23
|
anbi12d |
|- ( x = ( y + A ) -> ( ( x e. CC /\ ( x - A ) e. B ) <-> ( ( y + A ) e. CC /\ ( ( y + A ) - A ) e. B ) ) ) |
25 |
20 24
|
syl5ibrcom |
|- ( ( ( A e. CC /\ B C_ CC ) /\ y e. B ) -> ( x = ( y + A ) -> ( x e. CC /\ ( x - A ) e. B ) ) ) |
26 |
25
|
rexlimdva |
|- ( ( A e. CC /\ B C_ CC ) -> ( E. y e. B x = ( y + A ) -> ( x e. CC /\ ( x - A ) e. B ) ) ) |
27 |
10 26
|
impbid |
|- ( ( A e. CC /\ B C_ CC ) -> ( ( x e. CC /\ ( x - A ) e. B ) <-> E. y e. B x = ( y + A ) ) ) |
28 |
27
|
abbidv |
|- ( ( A e. CC /\ B C_ CC ) -> { x | ( x e. CC /\ ( x - A ) e. B ) } = { x | E. y e. B x = ( y + A ) } ) |
29 |
1 28
|
eqtrid |
|- ( ( A e. CC /\ B C_ CC ) -> { x e. CC | ( x - A ) e. B } = { x | E. y e. B x = ( y + A ) } ) |