Theorem assintopval

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

	Ref	Expression
Assertion	assintopval	⊢ ( 𝑀 ∈ 𝑉 → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } )

Proof

Step	Hyp	Ref	Expression
1		df-assintop	⊢ assIntOp = ( 𝑚 ∈ V ↦ { 𝑜 ∈ ( clIntOp ‘ 𝑚 ) ∣ 𝑜 assLaw 𝑚 } )
2		fveq2	⊢ ( 𝑚 = 𝑀 → ( clIntOp ‘ 𝑚 ) = ( clIntOp ‘ 𝑀 ) )
3		breq2	⊢ ( 𝑚 = 𝑀 → ( 𝑜 assLaw 𝑚 ↔ 𝑜 assLaw 𝑀 ) )
4	2 3	rabeqbidv	⊢ ( 𝑚 = 𝑀 → { 𝑜 ∈ ( clIntOp ‘ 𝑚 ) ∣ 𝑜 assLaw 𝑚 } = { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } )
5		elex	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
6		fvex	⊢ ( clIntOp ‘ 𝑀 ) ∈ V
7	6	rabex	⊢ { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } ∈ V
8	7	a1i	⊢ ( 𝑀 ∈ 𝑉 → { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } ∈ V )
9	1 4 5 8	fvmptd3	⊢ ( 𝑀 ∈ 𝑉 → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } )