Theorem iscllaw

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

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

Proof

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