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 e. V /\ B e. W ) -> ( x e. A , y e. B |-> C ) e. _V )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
2 1 mpoexg 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. A , y e. B |-> C ) e. _V )