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 e. _V
	mpoex.2	|- B e. _V
Assertion	mpoex	|- ( x e. A , y e. B |-> C ) e. _V

Proof

Step	Hyp	Ref	Expression
1		mpoex.1	|- A e. _V
2		mpoex.2	|- B e. _V
3	2	rgenw	|- A. x e. A B e. _V
4		eqid	|- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
5	4	mpoexxg	|- ( ( A e. _V /\ A. x e. A B e. _V ) -> ( x e. A , y e. B |-> C ) e. _V )
6	1 3 5	mp2an	|- ( x e. A , y e. B |-> C ) e. _V