Metamath Proof Explorer

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 \in V \to assIntOp (M) = \{o \in (M^{(M \times M)}) \| o assLaw M\}$

Step	Hyp	Ref	Expression
1		assintopval	$⊢ M \in V \to assIntOp (M) = \{o \in clIntOp (M) \| o assLaw M\}$
2		clintopval	$⊢ M \in V \to clIntOp (M) = M^{(M \times M)}$
3	2	rabeqdv	$⊢ M \in V \to \{o \in clIntOp (M) \| o assLaw M\} = \{o \in (M^{(M \times M)}) \| o assLaw M\}$
4	1 3	eqtrd	$⊢ M \in V \to assIntOp (M) = \{o \in (M^{(M \times M)}) \| o assLaw M\}$