This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cntzsnval

Description: Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses cntzfval.b 
|- B = ( Base ` M )
cntzfval.p 
|- .+ = ( +g ` M )
cntzfval.z 
|- Z = ( Cntz ` M )
Assertion cntzsnval 
|- ( Y e. B -> ( Z ` { Y } ) = { x e. B | ( x .+ Y ) = ( Y .+ x ) } )

Proof

Step Hyp Ref Expression
1 cntzfval.b 
 |-  B = ( Base ` M )
2 cntzfval.p 
 |-  .+ = ( +g ` M )
3 cntzfval.z 
 |-  Z = ( Cntz ` M )
4 snssi 
 |-  ( Y e. B -> { Y } C_ B )
5 1 2 3 cntzval 
 |-  ( { Y } C_ B -> ( Z ` { Y } ) = { x e. B | A. y e. { Y } ( x .+ y ) = ( y .+ x ) } )
6 4 5 syl 
 |-  ( Y e. B -> ( Z ` { Y } ) = { x e. B | A. y e. { Y } ( x .+ y ) = ( y .+ x ) } )
7 oveq2 
 |-  ( y = Y -> ( x .+ y ) = ( x .+ Y ) )
8 oveq1 
 |-  ( y = Y -> ( y .+ x ) = ( Y .+ x ) )
9 7 8 eqeq12d 
 |-  ( y = Y -> ( ( x .+ y ) = ( y .+ x ) <-> ( x .+ Y ) = ( Y .+ x ) ) )
10 9 ralsng 
 |-  ( Y e. B -> ( A. y e. { Y } ( x .+ y ) = ( y .+ x ) <-> ( x .+ Y ) = ( Y .+ x ) ) )
11 10 rabbidv 
 |-  ( Y e. B -> { x e. B | A. y e. { Y } ( x .+ y ) = ( y .+ x ) } = { x e. B | ( x .+ Y ) = ( Y .+ x ) } )
12 6 11 eqtrd 
 |-  ( Y e. B -> ( Z ` { Y } ) = { x e. B | ( x .+ Y ) = ( Y .+ x ) } )