Step |
Hyp |
Ref |
Expression |
1 |
|
cntzfval.b |
|- B = ( Base ` M ) |
2 |
|
cntzfval.p |
|- .+ = ( +g ` M ) |
3 |
|
cntzfval.z |
|- Z = ( Cntz ` M ) |
4 |
1 2 3
|
cntzval |
|- ( S C_ B -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) |
5 |
4
|
eleq2d |
|- ( S C_ B -> ( A e. ( Z ` S ) <-> A e. { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) ) |
6 |
|
oveq1 |
|- ( x = A -> ( x .+ y ) = ( A .+ y ) ) |
7 |
|
oveq2 |
|- ( x = A -> ( y .+ x ) = ( y .+ A ) ) |
8 |
6 7
|
eqeq12d |
|- ( x = A -> ( ( x .+ y ) = ( y .+ x ) <-> ( A .+ y ) = ( y .+ A ) ) ) |
9 |
8
|
ralbidv |
|- ( x = A -> ( A. y e. S ( x .+ y ) = ( y .+ x ) <-> A. y e. S ( A .+ y ) = ( y .+ A ) ) ) |
10 |
9
|
elrab |
|- ( A e. { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } <-> ( A e. B /\ A. y e. S ( A .+ y ) = ( y .+ A ) ) ) |
11 |
5 10
|
bitrdi |
|- ( S C_ B -> ( A e. ( Z ` S ) <-> ( A e. B /\ A. y e. S ( A .+ y ) = ( y .+ A ) ) ) ) |