Theorem elcntzsn

Description: Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	cntzfval.b	|- B = ( Base ` M )
	cntzfval.p	|- .+ = ( +g ` M )
	cntzfval.z	|- Z = ( Cntz ` M )
Assertion	elcntzsn	|- ( Y e. B -> ( X e. ( 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	1 2 3	cntzsnval	|- ( Y e. B -> ( Z ` { Y } ) = { x e. B | ( x .+ Y ) = ( Y .+ x ) } )
5	4	eleq2d	|- ( Y e. B -> ( X e. ( Z ` { Y } ) <-> X e. { x e. B | ( x .+ Y ) = ( Y .+ x ) } ) )
6		oveq1	|- ( x = X -> ( x .+ Y ) = ( X .+ Y ) )
7		oveq2	|- ( x = X -> ( Y .+ x ) = ( Y .+ X ) )
8	6 7	eqeq12d	|- ( x = X -> ( ( x .+ Y ) = ( Y .+ x ) <-> ( X .+ Y ) = ( Y .+ X ) ) )
9	8	elrab	|- ( X e. { x e. B | ( x .+ Y ) = ( Y .+ x ) } <-> ( X e. B /\ ( X .+ Y ) = ( Y .+ X ) ) )
10	5 9	bitrdi	|- ( Y e. B -> ( X e. ( Z ` { Y } ) <-> ( X e. B /\ ( X .+ Y ) = ( Y .+ X ) ) ) )