Metamath Proof Explorer

Theorem mpoexga

Description: If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011)

		Ref	Expression
	Assertion	mpoexga	$⊢ (A \in V \land B \in W) \to (x \in A, y \in B ⟼ C) \in V$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (x \in A, y \in B ⟼ C) = (x \in A, y \in B ⟼ C)$
2	1	mpoexg	$⊢ (A \in V \land B \in W) \to (x \in A, y \in B ⟼ C) \in V$