Theorem assintopmap

Description: The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	assintopmap	|- ( M e. V -> ( assIntOp ` M ) = { o e. ( M ^m ( M X. M ) ) | o assLaw M } )

Proof

Step	Hyp	Ref	Expression
1		assintopval	|- ( M e. V -> ( assIntOp ` M ) = { o e. ( clIntOp ` M ) | o assLaw M } )
2		clintopval	|- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )
3	2	rabeqdv	|- ( M e. V -> { o e. ( clIntOp ` M ) | o assLaw M } = { o e. ( M ^m ( M X. M ) ) | o assLaw M } )
4	1 3	eqtrd	|- ( M e. V -> ( assIntOp ` M ) = { o e. ( M ^m ( M X. M ) ) | o assLaw M } )