Metamath Proof Explorer

Theorem mpoex

Description: If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013)

	Ref	Expression
Hypotheses	mpoex.1	$⊢ A \in V$
	mpoex.2	$⊢ B \in V$
Assertion	mpoex	$⊢ (x \in A, y \in B ⟼ C) \in V$

Proof

Step	Hyp	Ref	Expression
1		mpoex.1	$⊢ A \in V$
2		mpoex.2	$⊢ B \in V$
3	2	rgenw	$⊢ \forall x \in A B \in V$
4		eqid	$⊢ (x \in A, y \in B ⟼ C) = (x \in A, y \in B ⟼ C)$
5	4	mpoexxg	$⊢ (A \in V \land \forall x \in A B \in V) \to (x \in A, y \in B ⟼ C) \in V$
6	1 3 5	mp2an	$⊢ (x \in A, y \in B ⟼ C) \in V$