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 V B W x A , y B C V


Step Hyp Ref Expression
1 eqid x A , y B C = x A , y B C
2 1 mpoexg A V B W x A , y B C V