Theorem iscomlaw

Description: The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	iscomlaw	|- ( ( .o. e. V /\ M e. W ) -> ( .o. comLaw M <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( o = .o. /\ m = M ) -> m = M )
2		oveq	|- ( o = .o. -> ( x o y ) = ( x .o. y ) )
3		oveq	|- ( o = .o. -> ( y o x ) = ( y .o. x ) )
4	2 3	eqeq12d	|- ( o = .o. -> ( ( x o y ) = ( y o x ) <-> ( x .o. y ) = ( y .o. x ) ) )
5	4	adantr	|- ( ( o = .o. /\ m = M ) -> ( ( x o y ) = ( y o x ) <-> ( x .o. y ) = ( y .o. x ) ) )
6	1 5	raleqbidv	|- ( ( o = .o. /\ m = M ) -> ( A. y e. m ( x o y ) = ( y o x ) <-> A. y e. M ( x .o. y ) = ( y .o. x ) ) )
7	1 6	raleqbidv	|- ( ( o = .o. /\ m = M ) -> ( A. x e. m A. y e. m ( x o y ) = ( y o x ) <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) )
8		df-comlaw	|- comLaw = { <. o , m >. | A. x e. m A. y e. m ( x o y ) = ( y o x ) }
9	7 8	brabga	|- ( ( .o. e. V /\ M e. W ) -> ( .o. comLaw M <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) )