Metamath Proof Explorer


Theorem mpov

Description: Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013)

Ref Expression
Assertion mpov
|- ( x e. _V , y e. _V |-> C ) = { <. <. x , y >. , z >. | z = C }

Proof

Step Hyp Ref Expression
1 df-mpo
 |-  ( x e. _V , y e. _V |-> C ) = { <. <. x , y >. , z >. | ( ( x e. _V /\ y e. _V ) /\ z = C ) }
2 vex
 |-  x e. _V
3 vex
 |-  y e. _V
4 2 3 pm3.2i
 |-  ( x e. _V /\ y e. _V )
5 4 biantrur
 |-  ( z = C <-> ( ( x e. _V /\ y e. _V ) /\ z = C ) )
6 5 oprabbii
 |-  { <. <. x , y >. , z >. | z = C } = { <. <. x , y >. , z >. | ( ( x e. _V /\ y e. _V ) /\ z = C ) }
7 1 6 eqtr4i
 |-  ( x e. _V , y e. _V |-> C ) = { <. <. x , y >. , z >. | z = C }