Step |
Hyp |
Ref |
Expression |
1 |
|
elnmz.1 |
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) } |
2 |
|
oveq2 |
|- ( y = z -> ( x .+ y ) = ( x .+ z ) ) |
3 |
2
|
eleq1d |
|- ( y = z -> ( ( x .+ y ) e. S <-> ( x .+ z ) e. S ) ) |
4 |
|
oveq1 |
|- ( y = z -> ( y .+ x ) = ( z .+ x ) ) |
5 |
4
|
eleq1d |
|- ( y = z -> ( ( y .+ x ) e. S <-> ( z .+ x ) e. S ) ) |
6 |
3 5
|
bibi12d |
|- ( y = z -> ( ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) <-> ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) ) ) |
7 |
6
|
cbvralvw |
|- ( A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) <-> A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) ) |
8 |
|
oveq1 |
|- ( x = A -> ( x .+ z ) = ( A .+ z ) ) |
9 |
8
|
eleq1d |
|- ( x = A -> ( ( x .+ z ) e. S <-> ( A .+ z ) e. S ) ) |
10 |
|
oveq2 |
|- ( x = A -> ( z .+ x ) = ( z .+ A ) ) |
11 |
10
|
eleq1d |
|- ( x = A -> ( ( z .+ x ) e. S <-> ( z .+ A ) e. S ) ) |
12 |
9 11
|
bibi12d |
|- ( x = A -> ( ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) ) |
13 |
12
|
ralbidv |
|- ( x = A -> ( A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) ) |
14 |
7 13
|
syl5bb |
|- ( x = A -> ( A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) <-> A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) ) |
15 |
14 1
|
elrab2 |
|- ( A e. N <-> ( A e. X /\ A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) ) |