Theorem assintopval

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

	Ref	Expression
Assertion	assintopval	|- ( M e. V -> ( assIntOp ` M ) = { o e. ( clIntOp ` M ) | o assLaw M } )

Proof

Step	Hyp	Ref	Expression
1		df-assintop	|- assIntOp = ( m e. _V |-> { o e. ( clIntOp ` m ) | o assLaw m } )
2		fveq2	|- ( m = M -> ( clIntOp ` m ) = ( clIntOp ` M ) )
3		breq2	|- ( m = M -> ( o assLaw m <-> o assLaw M ) )
4	2 3	rabeqbidv	|- ( m = M -> { o e. ( clIntOp ` m ) | o assLaw m } = { o e. ( clIntOp ` M ) | o assLaw M } )
5		elex	|- ( M e. V -> M e. _V )
6		fvex	|- ( clIntOp ` M ) e. _V
7	6	rabex	|- { o e. ( clIntOp ` M ) | o assLaw M } e. _V
8	7	a1i	|- ( M e. V -> { o e. ( clIntOp ` M ) | o assLaw M } e. _V )
9	1 4 5 8	fvmptd3	|- ( M e. V -> ( assIntOp ` M ) = { o e. ( clIntOp ` M ) | o assLaw M } )