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 }