Theorem elnmz

Description: Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypothesis	elnmz.1	|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
Assertion	elnmz	|- ( A e. N <-> ( A e. X /\ A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) )

Proof

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	bitrid	|- ( 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 ) ) )