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 V
mpoex.2 B V
Assertion mpoex x A , y B C V


Step Hyp Ref Expression
1 mpoex.1 A V
2 mpoex.2 B V
3 2 rgenw x A B V
4 eqid x A , y B C = x A , y B C
5 4 mpoexxg A V x A B V x A , y B C V
6 1 3 5 mp2an x A , y B C V