assintopval

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

		Ref	Expression
	Assertion	assintopval	$⊢ M \in V \to assIntOp (M) = \{o \in clIntOp (M) \| o assLaw M\}$

Step	Hyp	Ref	Expression
1		df-assintop	$⊢ assIntOp = (m \in V ⟼ \{o \in clIntOp (m) \| o assLaw m\})$
2		fveq2	$⊢ m = M \to clIntOp (m) = clIntOp (M)$
3		breq2	$⊢ m = M \to (o assLaw m \leftrightarrow o assLaw M)$
4	2 3	rabeqbidv	$⊢ m = M \to \{o \in clIntOp (m) \| o assLaw m\} = \{o \in clIntOp (M) \| o assLaw M\}$
5		elex	$⊢ M \in V \to M \in V$
6		fvex	$⊢ clIntOp (M) \in V$
7	6	rabex	$⊢ \{o \in clIntOp (M) \| o assLaw M\} \in V$
8	7	a1i	$⊢ M \in V \to \{o \in clIntOp (M) \| o assLaw M\} \in V$
9	1 4 5 8	fvmptd3	$⊢ M \in V \to assIntOp (M) = \{o \in clIntOp (M) \| o assLaw M\}$

Metamath Proof Explorer