Metamath Proof Explorer

Theorem assintopval

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

Ref Expression
Assertion assintopval ⊢ M ∈ V → assIntOp ⁡ M = o ∈ clIntOp ⁡ M | o assLaw M

Proof

Step Hyp Ref Expression
1 df-assintop ⊢ assIntOp = m ∈ V ⟼ o ∈ 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 ∈ clIntOp ⁡ m | o assLaw m = o ∈ clIntOp ⁡ M | o assLaw M
5 elex ⊢ M ∈ V → M ∈ V
6 fvex ⊢ clIntOp ⁡ M ∈ V
7 6 rabex ⊢ o ∈ clIntOp ⁡ M | o assLaw M ∈ V
8 7 a1i ⊢ M ∈ V → o ∈ clIntOp ⁡ M | o assLaw M ∈ V
9 1 4 5 8 fvmptd3 ⊢ M ∈ V → assIntOp ⁡ M = o ∈ clIntOp ⁡ M | o assLaw M